diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs --- a/examples/simple-arith-core.hs +++ b/examples/simple-arith-core.hs @@ -27,7 +27,11 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 import qualified Data.Type.Ord as DTO #endif +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904 +import Data.Type.Bool +#endif + main :: IO () main = putStrLn "finished" @@ -131,4 +135,24 @@ maxLeq :: n <= m => NProxy n -> NProxy m -> DTO.Max n m :~: m maxLeq _ _ = Refl +#endif + +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904 +leqGeqToEq :: NProxy n -> NProxy m -> IsTrue (n <=? m && m <=? n) -> n :~: m +leqGeqToEq _ _ Witness = Refl + +leqTotal :: NProxy n -> NProxy m -> IsTrue (n <=? m || m <=? n) +leqTotal _ _ = Witness + +zeroMinimal :: NProxy n -> (n DTO. IsTrue (Not (n DTO. IsTrue (If (n DTO.<=? 0) (n == 0) (n DTO.>? 0)) +caseZero _ = Witness + +succGtZero :: NProxy n -> IsTrue (0 DTO. package moves to . - . - You can use by adding this package to @build-depends@ and add the following pragma - to the head of .hs files: - . - . - > OPTIONS_GHC -fplugin GHC.TypeLits.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 +name: ghc-typelits-presburger +version: 0.7.0.0 +synopsis: Presburger Arithmetic Solver for GHC Type-level natural numbers. +description: @ghc-typelits-presburger@ augments GHC type-system with Presburger + Arithmetic Solver for Type-level natural numbers. + This plugin only work with GHC builtin operations. + To work with those of @singletons@ package, use @ghc-typelits-meta@ and/or @ghc-typelits-presburger@ instead. + . + Since 0.3.0.0, integration with package moves to . + . + You can use by adding this package to @build-depends@ and add the following pragma + to the head of .hs files: + . + . + > OPTIONS_GHC -fplugin GHC.TypeLits.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 tested-with: - GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.1 GHC==9.2.1 -build-type: Simple + GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.2 GHC==9.2.4 GHC==9.4.3 +build-type: Simple source-repository head type: git @@ -56,7 +56,7 @@ build-depends: base >=4.7 && <5 , containers - , ghc <9.3 + , ghc <9.5 , ghc-tcplugins-extra >=0.2 && <0.5 , mtl , pretty @@ -76,9 +76,9 @@ base , equational-reasoning , ghc-typelits-presburger + default-language: Haskell2010 if !(flag(examples)) buildable: False - default-language: Haskell2010 test-suite test-typeltis-presburger type: exitcode-stdio-1.0 diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs --- a/src/GHC/TypeLits/Presburger/Compat.hs +++ b/src/GHC/TypeLits/Presburger/Compat.hs @@ -10,8 +10,19 @@ import Data.Generics.Twins #if MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS, dATA_TYPE_EQUALITY) +import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS) +#if MIN_VERSION_ghc(9,4,1) +import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..)) +#else +import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..)) +#endif +#if MIN_VERSION_ghc(9,4,1) +import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (mkBaseModule, gHC_TYPEERROR) +import GHC.Core.Reduction (reductionReducedType) +#else +import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (dATA_TYPE_EQUALITY) import qualified GHC.Builtin.Names as Old +#endif import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule(..), NoExtField(..)) import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl(..), ImportDeclQualifiedStyle(..)) import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs) @@ -104,7 +115,7 @@ tcPluginIO, tcPluginTrace, ) -import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..)) +import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..)) import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat ( Ct, CtEvidence, @@ -209,6 +220,15 @@ #endif #endif +#if !MIN_VERSION_ghc(9,4,1) +type TcPluginSolveResult = TcPluginResult +#endif + +#if MIN_VERSION_ghc(9,4,1) +dATA_TYPE_EQUALITY :: Module +dATA_TYPE_EQUALITY = mkBaseModule "Data.Type.Equality" +#endif + #if MIN_VERSION_ghc(8,10,1) type PredTree = Pred #endif @@ -368,10 +388,19 @@ type RawUnitId = FastString preloadedUnitsM :: TcPluginM [FastString] -#if MIN_VERSION_ghc(9,2,0) +#if MIN_VERSION_ghc(9,4,0) preloadedUnitsM = do logger <- unsafeTcPluginTcM getLogger dflags <- hsc_dflags <$> getTopEnv + packs <- tcPluginIO $ initUnits logger dflags Nothing mempty <&> + \(_, us, _, _ ) -> preloadUnits us + let packNames = map (\(UnitId p) -> p) packs + tcPluginTrace "pres: packs" $ ppr packNames + pure packNames +#elif MIN_VERSION_ghc(9,2,0) +preloadedUnitsM = do + logger <- unsafeTcPluginTcM getLogger + dflags <- hsc_dflags <$> getTopEnv packs <- tcPluginIO $ initUnits logger dflags Nothing <&> \(_, us, _, _ ) -> preloadUnits us let packNames = map (\(UnitId p) -> p) packs @@ -464,6 +493,15 @@ pure typeNatLeqTyCon #endif +lookupAssertTyCon :: TcPluginM (Maybe TyCon) +#if MIN_VERSION_base(4,17,0) +lookupAssertTyCon = + fmap Just . tcLookupTyCon =<< lookupOrig gHC_TYPEERROR (mkTcOcc "Assert") +#else +lookupAssertTyCon = pure Nothing +#endif + + lookupTyNatPredLt :: TcPluginM (Maybe TyCon) -- Note: base library shipepd with 9.2.1 has a wrong implementation; -- hence we MUST NOT desugar it with <= 9.2.1 @@ -536,4 +574,27 @@ tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc "Compare") #else lookupTyGenericCompare = pure Nothing +#endif + + +lookupBool47 :: String -> TcPluginM (Maybe TyCon) +#if MIN_VERSION_base(4,17,0) +lookupBool47 nam = Just <$> do + tcLookupTyCon =<< lookupOrig (mkBaseModule "Data.Type.Bool") (mkTcOcc nam) +#else +lookupBool47 = const $ pure Nothing +#endif + +lookupTyNot, lookupTyIf, lookupTyAnd, lookupTyOr :: TcPluginM (Maybe TyCon) +lookupTyNot = lookupBool47 "Not" +lookupTyIf = lookupBool47 "If" +lookupTyAnd = lookupBool47 "&&" +lookupTyOr = lookupBool47 "||" + + +matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe Type) +#if MIN_VERSION_ghc(9,4,1) +matchFam' con args = fmap reductionReducedType <$> matchFam con args +#else +matchFam' con args = fmap snd <$> matchFam con args #endif diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs --- a/src/GHC/TypeLits/Presburger/Types.hs +++ b/src/GHC/TypeLits/Presburger/Types.hs @@ -15,6 +15,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DerivingVia #-} +{-# LANGUAGE NamedFieldPuns #-} -- | Since 0.3.0.0 module GHC.TypeLits.Presburger.Types ( pluginWith, @@ -114,8 +115,16 @@ "typelits-presburger" TcPlugin { tcPluginInit = return () - , tcPluginSolve = decidePresburger mode trans , tcPluginStop = const $ return () +#if MIN_VERSION_ghc(9,4,1) + , tcPluginSolve = const $ \_ gs ws -> decidePresburger mode trans () gs [] ws +#else + , tcPluginSolve = decidePresburger mode trans +#endif + +#if MIN_VERSION_ghc(9,4,1) + , tcPluginRewrite = mempty +#endif } testIf :: PropSet -> Prop -> Proof @@ -167,6 +176,7 @@ data Translation = Translation { isEmpty :: [TyCon] , ordCond :: [TyCon] + , assertTy :: [TyCon] , isTrue :: [TyCon] , trueData :: [TyCon] , falseData :: [TyCon] @@ -174,6 +184,10 @@ , tyEq :: [TyCon] , tyEqBool :: [TyCon] , tyEqWitness :: [TyCon] + , tyNot :: [TyCon] + , tyAnd :: [TyCon] + , tyOr :: [TyCon] + , tyIf :: [TyCon] , tyNeqBool :: [TyCon] , natPlus :: [TyCon] , natMinus :: [TyCon] @@ -202,8 +216,13 @@ Translation { isEmpty = isEmpty l <> isEmpty r , isTrue = isTrue l <> isTrue r + , assertTy = assertTy l <> assertTy r , voids = voids l <> voids r , tyEq = tyEq l <> tyEq r + , tyNot = tyNot l <> tyNot r + , tyAnd = tyAnd l <> tyAnd r + , tyOr = tyOr l <> tyOr r + , tyIf = tyIf l <> tyIf r , tyEqBool = tyEqBool l <> tyEqBool r , tyEqWitness = tyEqWitness l <> tyEqWitness r , tyNeqBool = tyNeqBool l <> tyNeqBool r @@ -237,10 +256,15 @@ Translation { isEmpty = mempty , isTrue = mempty + , assertTy = mempty , tyEq = mempty , tyEqBool = mempty , tyEqWitness = mempty , tyNeqBool = mempty + , tyNot = mempty + , tyAnd = mempty + , tyOr = mempty + , tyIf = mempty , voids = mempty , natPlus = mempty , natMinus = mempty @@ -267,7 +291,7 @@ , ordCond = mempty } -decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult +decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult decidePresburger _ genTrans _ gs [] [] = do tcPluginTrace "pres: Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs) trans <- genTrans @@ -287,7 +311,6 @@ tcPluginTrace "pres: Current subst" (ppr subst) tcPluginTrace "pres: wanteds" $ ppr $ map (subsType subst . deconsPred . subsCt subst) ws tcPluginTrace "pres: givens" $ ppr $ map (subsType subst . deconsPred) gs - tcPluginTrace "pres: deriveds" $ ppr $ map deconsPred _ds (prems, wants, prems0) <- do wants <- catMaybes @@ -355,6 +378,7 @@ eqTyCon_ <- getEqTyCon eqBoolTyCon <- tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc "==") eqWitCon_ <- getEqWitnessTyCon + assertTy <- lookupAssertTyCon vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base") voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void") nLeq <- tcLookupTyCon =<< lookupTyNatPredLeq @@ -367,10 +391,19 @@ mTyGtB <- lookupTyNatBoolGt mOrdCond <- mOrdCondTyCon mtyGenericCompare <- lookupTyGenericCompare + tyNot <- maybeToList <$> lookupTyNot + tyAnd <- maybeToList <$> lookupTyAnd + tyOr <- maybeToList <$> lookupTyOr + tyIf <- maybeToList <$> lookupTyIf let trans = mempty { isEmpty = isEmpties + , assertTy = maybeToList assertTy , tyEq = [eqTyCon_] + , tyNot + , tyAnd + , tyOr + , tyIf , ordCond = F.toList mOrdCond , tyEqWitness = [eqWitCon_] , tyEqBool = [eqBoolTyCon] @@ -401,12 +434,6 @@ (<=>) :: Prop -> Prop -> Prop p <=> q = (p :&& q) :|| (Not p :&& Not q) -withEv :: Ct -> (EvTerm, Ct) -withEv ct = - case classifyPredType (deconsPred ct) of - EqPred _ t1 t2 -> (evByFiat "ghc-typelits-presburger" t1 t2, ct) - _ -> error $ "UnknownPredEv: " <> showSDocUnsafe (ppr ct) - orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)] orderingDic = [(lt, (:<)) | lt <- orderingLT given] @@ -420,6 +447,8 @@ toPresburgerPred (TyConApp con (lastN 2 -> [t1, t2])) | con `elem` (natLeq given ++ natLeqBool given) = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 +toPresburgerPred (TyConApp con [t1, _]) + | con `elem` assertTy given = toPresburgerPred t1 toPresburgerPred ty | Just (con, []) <- splitTyConApp_maybe ty , con `elem` trueData given = @@ -442,6 +471,21 @@ | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l => , con `elem` isTrue given = toPresburgerPred l + | Just (con, [l]) <- splitTyConApp_maybe ty -- Not p (from Data.Type.Bool) + , con `elem` tyNot given = + Not <$> toPresburgerPred l + | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p && q (from Data.Type.Bool) + , con `elem` tyAnd given = + (:&&) <$> toPresburgerPred l <*> toPresburgerPred r + | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p || q (from Data.Type.Bool) + , con `elem` tyOr given = + (:||) <$> toPresburgerPred l <*> toPresburgerPred r + | Just (con, lastN 3 -> [p, t, f]) <- splitTyConApp_maybe ty -- If p t f (from Data.Type.Bool) + , con `elem` tyIf given = do + p' <- toPresburgerPred p + (:||) + <$> ((p' :&&) <$> toPresburgerPred t) + <*> ((Not p':&&) <$> toPresburgerPred f) | Just (con, [t1, t2]) <- splitTyConAppLastBin ty , typeKind t1 `eqType` typeNatKind , typeKind t2 `eqType` typeNatKind @@ -601,6 +645,9 @@ toPresburgerExp :: Given Translation => Type -> Machine Expr toPresburgerExp ty = case ty of TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t + TyConApp tc (lastN 3 -> [p, t, f]) + | tc `elem` tyIf given -> + If <$> toPresburgerPred p <*> toPresburgerExp t <*> toPresburgerExp f TyConApp tc (lastN 4 -> [cmpNM, l, e, g]) | tc `elem` ordCond given , TyConApp cmp (lastN 2 -> [n, m]) <- cmpNM diff --git a/test/GHC/TypeLits/PresburgerSpec.hs b/test/GHC/TypeLits/PresburgerSpec.hs --- a/test/GHC/TypeLits/PresburgerSpec.hs +++ b/test/GHC/TypeLits/PresburgerSpec.hs @@ -21,6 +21,9 @@ case eith of Left (TypeError msg) | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" + `T.isInfixOf` T.pack msg + || + "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)" `T.isInfixOf` T.pack msg -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith @@ -29,6 +32,8 @@ case eith of Left (TypeError msg) | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" + `T.isInfixOf` T.pack msg + || "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)" `T.isInfixOf` T.pack msg -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith @@ -43,7 +48,10 @@ case eith of Left (TypeError msg) | "Could not deduce: n1 ~ n" - `T.isInfixOf` T.pack msg -> + `T.isInfixOf` T.pack msg + || "Could not deduce (n1 ~ n)" + `T.isInfixOf` T.pack msg + -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith , testCase "With plugin" $ do @@ -51,6 +59,9 @@ case eith of Left (TypeError msg) | "Could not deduce: n1 ~ n" + `T.isInfixOf` T.pack msg + || + "Could not deduce (n1 ~ n)" `T.isInfixOf` T.pack msg -> pure () _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith