diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs --- a/examples/simple-arith.hs +++ b/examples/simple-arith.hs @@ -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 diff --git a/singletons-presburger.cabal b/singletons-presburger.cabal --- a/singletons-presburger.cabal +++ b/singletons-presburger.cabal @@ -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 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 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 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 @@ -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