singletons-presburger 0.7.4.0 → 0.7.4.1
raw patch · 3 files changed
+247/−96 lines, 3 filesdep +transformersPVP: minor bump suggested
API additions: PVP suggests at least a minor version bump
Dependencies added: transformers
API changes (from Hackage documentation)
+ Data.Singletons.TypeNats.Presburger: instance GHC.Classes.Eq Data.Singletons.TypeNats.Presburger.ComparisonMethod
+ Data.Singletons.TypeNats.Presburger: instance GHC.Utils.Outputable.Outputable Data.Singletons.TypeNats.Presburger.ComparisonMethod
Files
- examples/simple-arith.hs +1/−2
- singletons-presburger.cabal +68/−58
- src/Data/Singletons/TypeNats/Presburger.hs +178/−36
examples/simple-arith.hs view
@@ -8,11 +8,10 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE NoStarIsType #-}-{-# OPTIONS_GHC -dcore-lint #-}+{-# OPTIONS_GHC -dcore-lint -ddump-tc-trace -ddump-to-file #-} {-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-} module Main where
singletons-presburger.cabal view
@@ -1,35 +1,33 @@-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: 7f7a8db05068df4e3d097d9d0d1cf27fa5c559de956d89dfa6cecb97d6561028+cabal-version: 3.4+name: singletons-presburger+version: 0.7.4.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.+ .+ You can use by adding this package to @dependencies@ and add the following pragma+ to the head of .hs files:+ .+ > OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger -name: singletons-presburger-version: 0.7.4.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.- .- You can use by adding this package to @dependencies@ and add the following pragma- to the head of .hs files:- .- > OPTIONS_GHC -fplugin Data.Singletons.TypeNats.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 tested-with:- GHC==9.2.8 GHC==9.4.8 GHC==9.6.5 GHC==9.8.2 GHC==9.10.1-extra-source-files:- Changelog.md-build-type: Simple+ ghc ==9.6.7+ ghc ==9.8.4+ ghc ==9.10.2+ ghc ==9.12.2 +extra-source-files: Changelog.md+build-type: Simple+ source-repository head type: git location: https://github.com/konn/ghc-typelits-presburger@@ -39,40 +37,52 @@ manual: False default: False +common defaults+ autogen-modules: Paths_singletons_presburger+ other-modules: Paths_singletons_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- exposed-modules:- Data.Singletons.TypeNats.Presburger- other-modules:- Paths_singletons_presburger- hs-source-dirs:- src- ghc-options: -Wall -Wno-dodgy-imports- cpp-options: -DSINGLETONS_BASE+ import: defaults+ exposed-modules: Data.Singletons.TypeNats.Presburger+ hs-source-dirs: src build-depends:- base >=4.7 && <5- , ghc- , ghc-typelits-presburger >=0.4- , mtl- , reflection- , singletons- , singletons-base >=3.0- default-language: Haskell2010+ base >=4.7 && <5,+ ghc,+ ghc-typelits-presburger >=0.4,+ mtl,+ reflection,+ singletons,+ singletons-base >=3.0,+ transformers, executable simple-arith+ import: defaults main-is: simple-arith.hs- other-modules:- Paths_singletons_presburger- hs-source-dirs:- examples- ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports- cpp-options: -DSINGLETONS_BASE+ hs-source-dirs: examples+ ghc-options:+ -Wall+ -Wno-dodgy-imports+ -Wno-unused-imports+ build-depends:- base- , equational-reasoning- , singletons- , singletons-base >=3.0- , singletons-presburger- , singletons-th- default-language: Haskell2010+ base,+ equational-reasoning,+ singletons,+ singletons-base >=3.0,+ singletons-presburger,+ singletons-th,+ if !(flag(examples)) buildable: False
src/Data/Singletons/TypeNats/Presburger.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE BlockArguments #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-}@@ -17,7 +18,11 @@ import Control.Monad import Control.Monad.Trans (MonadTrans (lift))+import Control.Monad.Trans.Maybe+import Data.Maybe (fromMaybe) import Data.Reflection (Given, give, given)+import qualified Debug.Trace as DT+import GHC.Plugins (Outputable, (<+>)) import GHC.TypeLits.Presburger.Compat import GHC.TypeLits.Presburger.Types @@ -27,7 +32,8 @@ (<>) <$> defaultTranslation <*> singletonTranslation data SingletonCons = SingletonCons- { singNatLeq :: TyCon+ { singApply :: TyCon+ , singNatLeq :: TyCon , singNatGeq :: TyCon , singNatLt :: TyCon , singNatGt :: TyCon@@ -37,16 +43,23 @@ , singNatCompare :: TyCon , singTrueSym0 :: TyCon , singFalseSym0 :: TyCon- , caseNameForSingLeq :: TyCon- , caseNameForSingGeq :: TyCon- , caseNameForSingLt :: TyCon- , caseNameForSingGt :: TyCon+ , caseNameForSingLeq :: [ComparisonMethod]+ , caseNameForSingGeq :: [ComparisonMethod]+ , caseNameForSingLt :: [ComparisonMethod]+ , caseNameForSingGt :: [ComparisonMethod] , singMin :: TyCon , singMax :: TyCon- , caseNameForMin :: TyCon- , caseNameForMax :: TyCon+ , caseNameForMin :: [ComparisonMethod]+ , caseNameForMax :: [ComparisonMethod] } +data ComparisonMethod = CaseFun TyCon | DirectTFHelper TyCon+ deriving (Eq)++instance Outputable ComparisonMethod where+ ppr (CaseFun con) = text "CaseFun" <+> ppr con+ ppr (DirectTFHelper con) = text "DirectTFHelper" <+> ppr con+ singletonTranslation :: TcPluginM Translation singletonTranslation = toTranslation <$> genSingletonCons@@ -72,32 +85,52 @@ , falseData = [singFalseSym0] } -singPackage :: FastString-singPackage = "singletons-base"+singBasePackage :: FastString+singBasePackage = "singletons-base" -ordModName, numModName, prelInstName :: ModuleName+singTopPackage :: FastString+singTopPackage = "singletons"++ordModName, numModName, prelInstName, dataSingletonsName :: ModuleName ordModName = mkModuleName "Data.Ord.Singletons" numModName = mkModuleName "GHC.Num.Singletons" prelInstName = mkModuleName "Data.Singletons.Base.Instances"+dataSingletonsName = mkModuleName "Data.Singletons" genSingletonCons :: TcPluginM SingletonCons genSingletonCons = do- singletonOrd <- lookupModule ordModName singPackage+ tcPluginTrace "sing: Start singleton consing" ""+ dataSingletons <- lookupModule dataSingletonsName singTopPackage+ singletonOrd <- lookupModule ordModName singBasePackage+ tcPluginTrace "sing: singletonOrd" $ ppr singletonOrd let singUnit = moduleUnit' singletonOrd prel = mkModule singUnit prelInstName singletonsNum = mkModule singUnit numModName+ singApply <- tcLookupTyCon =<< lookupOrig dataSingletons (mkTcOcc "Apply") singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")+ tcPluginTrace "sing: singTrueSym0" $ ppr singTrueSym0 singFalseSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "FalseSym0")+ tcPluginTrace "sing: singFalseSym0" $ ppr singFalseSym0 singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<=")+ tcPluginTrace "sing: singNatLeq" $ ppr singNatLeq singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<")+ tcPluginTrace "sing: singNatLt" $ ppr singNatLt singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ">=")+ tcPluginTrace "sing: singNatGeq" $ ppr singNatGeq singNatGt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ">")+ tcPluginTrace "sing: singNatGt" $ ppr singNatGt singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "+")+ tcPluginTrace "sing: singNatPlus" $ ppr singNatPlus singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "*")+ tcPluginTrace "sing: singNatTimes" $ ppr singNatTimes singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "-")+ tcPluginTrace "sing: singNatMinus" $ ppr singNatMinus singMin <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Min")+ tcPluginTrace "sing: singNatMin" $ ppr singMin singMax <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Max")+ tcPluginTrace "sing: singNatMax" $ ppr singMax caseNameForSingLeq <- getCaseNameForSingletonBinRel singNatLeq+ tcPluginTrace "sing: caseNameForSingLeq" $ ppr caseNameForSingLeq caseNameForSingLt <- getCaseNameForSingletonBinRel singNatLt caseNameForSingGeq <- getCaseNameForSingletonBinRel singNatGeq caseNameForSingGt <- getCaseNameForSingletonBinRel singNatGt@@ -108,29 +141,83 @@ ppr (singMin, singMax, caseNameForMin, caseNameForMax) return SingletonCons {..} -getCaseNameForSingletonBinOp :: TyCon -> TcPluginM TyCon-getCaseNameForSingletonBinOp con = do+getCaseNameForSingletonBinOp :: TyCon -> TcPluginM [ComparisonMethod]+#if MIN_VERSION_singletons_base(3,5,0)+getCaseNameForSingletonBinOp = getCaseNameForSingletonBinOpSingleton35+#else+getCaseNameForSingletonBinOp = getCaseNameForSingletonBinOpOldSingleton+#endif++getCaseNameForSingletonBinOpSingleton35 :: TyCon -> TcPluginM [ComparisonMethod]+getCaseNameForSingletonBinOpSingleton35 con = do let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)] tcPluginTrace "matching... for " (ppr con)+ matched <- fmap splitTyConApp <$> matchFam' con vars+ tcPluginTrace "matched. " (ppr matched)+ Just (appTy0, [n, l, r]) <- fmap splitTyConApp <$> matchFam' con vars+ applied <- matchFam' appTy0 [n, l, r]+ tcPluginTrace "Double matched. " (ppr $ splitTyConApp_maybe =<< applied)+ rest <-+ fromMaybe [] <$> runMaybeT do+ (app, args@[_bool, _nat, _body, _comps]) <- hoistMaybe $ splitTyConApp_maybe =<< applied+ lift $ tcPluginTrace "app, args" (ppr (app, args))+ agains <- MaybeT (matchFam' app args)+ lift $ tcPluginTrace "Final match" (ppr agains)+ (caseName, [_N, _0, _02, _]) <-+ hoistMaybe $ splitTyConApp_maybe agains+ pure [CaseFun caseName]+ return $ DirectTFHelper appTy0 : rest++getCaseNameForSingletonBinOpOldSingleton :: TyCon -> TcPluginM [ComparisonMethod]+getCaseNameForSingletonBinOpOldSingleton con = do+ let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]+ tcPluginTrace "matching... for " (ppr con) Just (appTy0, [n, b, bdy, r]) <- fmap splitTyConApp <$> matchFam' con vars let (appTy, args) = splitTyConApp bdy Just innermost <- matchFam' appTy args Just dat <- matchFam' appTy0 [n, b, innermost, r] Just dat' <- uncurry matchFam' (splitTyConApp dat)- let Just (con', _) = splitTyConApp_maybe dat'- return con'+ tcPluginTrace "matched. (orig, inner) = " (ppr (con, fst $ splitTyConApp dat'))+ return [CaseFun $ fst $ splitTyConApp dat'] -getCaseNameForSingletonBinRel :: TyCon -> TcPluginM TyCon-getCaseNameForSingletonBinRel con = do+getCaseNameForSingletonBinRel :: TyCon -> TcPluginM [ComparisonMethod]+#if MIN_VERSION_singletons_base(3,5,0)+getCaseNameForSingletonBinRel = getCaseNameForSingletonBinRelSingleton35+#else+getCaseNameForSingletonBinRel =getCaseNameForSingletonBinRelOldSingleton+#endif++getCaseNameForSingletonBinRelSingleton35 :: TyCon -> TcPluginM [ComparisonMethod]+getCaseNameForSingletonBinRelSingleton35 con = do let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)] tcPluginTrace "matching... for " (ppr con)+ matched <- fmap splitTyConApp <$> matchFam' con vars+ tcPluginTrace "matched. " (ppr matched)+ Just (appTy0, [n, l, r]) <- fmap splitTyConApp <$> matchFam' con vars+ applied <- matchFam' appTy0 [n, l, r]+ tcPluginTrace "Double matched. " (ppr $ splitTyConApp_maybe =<< applied)+ rest <-+ fromMaybe [] <$> runMaybeT do+ (app, args@[_ordering, _bool, _body, _comps]) <- hoistMaybe $ splitTyConApp_maybe =<< applied+ lift $ tcPluginTrace "app, args" (ppr (app, args))+ agains <- MaybeT (matchFam' app args)+ lift $ tcPluginTrace "Final match" (ppr agains)+ (caseName, [_N, _0, _02, _]) <-+ hoistMaybe $ splitTyConApp_maybe agains+ pure [CaseFun caseName]+ return $ DirectTFHelper appTy0 : rest++getCaseNameForSingletonBinRelOldSingleton :: TyCon -> TcPluginM [ComparisonMethod]+getCaseNameForSingletonBinRelOldSingleton con = do+ let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]+ tcPluginTrace "matching... for " (ppr con) Just (appTy0, [n, b, bdy, r]) <- fmap splitTyConApp <$> matchFam' con vars let (appTy, args) = splitTyConApp bdy Just innermost <- matchFam' appTy args Just dat <- matchFam' appTy0 [n, b, innermost, r] Just dat' <- uncurry matchFam' (splitTyConApp dat)- tcPluginTrace "matched. (orig, inner) = " (ppr (con, fst $ splitTyConApp dat'))- return $ fst $ splitTyConApp dat'+ tcPluginTrace "matched. (orig, inner)<= = " (ppr (con, fst $ splitTyConApp dat'))+ return [CaseFun $ fst $ splitTyConApp dat'] lastTwo :: [a] -> [a] lastTwo = drop <$> subtract 2 . length <*> id@@ -141,19 +228,27 @@ Type -> Machine Expr parseSingExpr toE ty+ -- singletons >=3.5+ | Just (con, [l, r]) <- splitTyConApp_maybe ty+ , Just bin <- lookup (DirectTFHelper con) minLikeCaseDic = do+ lift $ lift $ tcPluginTrace "hit!" $ ppr (ty, con)+ bin <$> toE l <*> toE r+ -- singletons <3.5 | Just (con, [_, l, r, _]) <- splitTyConApp_maybe ty- , Just bin <- lookup con minLikeCaseDic = do+ , Just bin <- lookup (CaseFun 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 -minLikeCaseDic :: (Given SingletonCons) => [(TyCon, Expr -> Expr -> Expr)]+minLikeCaseDic :: (Given SingletonCons) => [(ComparisonMethod, Expr -> Expr -> Expr)] minLikeCaseDic =- [ (caseNameForMin given, Min)- , (caseNameForMax given, Max)- ]+ concatMap+ (\(methods, op) -> [(method, op) | method <- methods])+ [ (caseNameForMin given, Min)+ , (caseNameForMax given, Max)+ ] parseSingPred :: (Given SingletonCons) =>@@ -162,22 +257,45 @@ Machine Prop 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] =+ | Just (con, [l, r]) <- splitTyConApp_maybe ty+ , Just bin <- lookup (DirectTFHelper con) compCaseDic = bin <$> toExp l <*> toExp r+ | Just (con, [_, _, l, r, cmpTy]) <- splitTyConApp_maybe ty+ , Just bin <- lookup (CaseFun con) compCaseDic+ , isCompTy cmpTy =+ bin <$> toExp l <*> toExp r+ | Just (con, [_, l, r, cmpTy]) <- splitTyConApp_maybe ty+ , Just bin <- lookup (CaseFun con) compCaseDic+ , isCompTy cmpTy =+ bin <$> toExp l <*> toExp r | otherwise = do lift $ lift $ tcPluginTrace "pres: Miokuring" (ppr ty) mzero -compCaseDic :: (Given SingletonCons) => [(TyCon, Expr -> Expr -> Prop)]+isCompTy :: (Given SingletonCons) => Type -> Bool+isCompTy cmpTy =+ case splitTyConApp_maybe cmpTy of+ Just (app, [_dom, _cod, f, _r])+ | app == singApply given+ , Just (app', [_dom', _cod', cmp, _l]) <- splitTyConApp_maybe f+ , app' == singApply given+ , Just (cmp', []) <- splitTyConApp_maybe cmp ->+ cmp' `elem` comps+ Just (cmp, _) ->+ cmp `elem` comps+ _ -> False+ where+ comps = [singNatCompare given, typeNatCmpTyCon]++compCaseDic :: (Given SingletonCons) => [(ComparisonMethod, Expr -> Expr -> Prop)] compCaseDic =- [ (caseNameForSingLeq given, (:<=))- , (caseNameForSingLt given, (:<))- , (caseNameForSingGeq given, (:>=))- , (caseNameForSingGt given, (:>))- ]+ concatMap+ (\(methods, op) -> [(method, op) | method <- methods])+ [ (caseNameForSingLeq given, (:<=))+ , (caseNameForSingLt given, (:<))+ , (caseNameForSingGeq given, (:>=))+ , (caseNameForSingGt given, (:>))+ ] parseSingPredTree :: (Given SingletonCons) =>@@ -185,16 +303,40 @@ PredTree -> Machine Prop parseSingPredTree toExp (EqPred NomEq p b) -- (n :<=? m) ~ 'True++ -- singletons >=3.5 | Just promotedTrueDataCon == tyConAppTyCon_maybe b -- Singleton's <=...+ , Just (con, [l, r]) <- splitTyConApp_maybe p+ , Just bin <- lookup (DirectTFHelper con) compCaseDic =+ bin <$> toExp l <*> toExp r+ | Just promotedFalseDataCon == tyConAppTyCon_maybe b -- Singleton's <=...+ , Just (con, [l, r]) <- splitTyConApp_maybe p+ , Just bin <- lookup (DirectTFHelper con) compCaseDic =+ fmap Not . bin <$> toExp l <*> toExp r+ -- singletons <3.5+ | Just promotedTrueDataCon == tyConAppTyCon_maybe b -- Singleton's <=... , Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe p- , Just bin <- lookup con compCaseDic+ , Just bin <- lookup (CaseFun 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 bin <- lookup (CaseFun con) compCaseDic , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =+ fmap Not . bin <$> toExp l <*> toExp r+ | Just promotedTrueDataCon == tyConAppTyCon_maybe b -- Singleton's <=...+ , Just (con, [_nat, l, r, cmpTy]) <- splitTyConApp_maybe p+ , Just bin <- lookup (CaseFun con) compCaseDic+ , DT.trace ("bin: " <> showSDocUnsafe (ppr con)) True+ , Just (cmp, _) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =+ bin <$> toExp l <*> toExp r+ | Just promotedFalseDataCon == tyConAppTyCon_maybe b -- Singleton's <=...+ , Just (con, [_nat, l, r, cmpTy]) <- splitTyConApp_maybe p+ , Just bin <- lookup (CaseFun con) compCaseDic+ , Just (cmp, _) <- splitTyConApp_maybe cmpTy , cmp `elem` [singNatCompare given, typeNatCmpTyCon] = fmap Not . bin <$> toExp l <*> toExp r parseSingPredTree _ _ = mzero