ghc-typelits-presburger 0.3.0.0 → 0.3.0.1
raw patch · 3 files changed
+79/−26 lines, 3 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
+ GHC.TypeLits.Presburger.Compat: mkPrimEqPredRole :: Role -> Type -> Type -> PredType
- GHC.TypeLits.Presburger.Compat: classifyPredType :: PredType -> PredTree
+ GHC.TypeLits.Presburger.Compat: classifyPredType :: Type -> PredTree
Files
- ghc-typelits-presburger.cabal +5/−5
- src/GHC/TypeLits/Presburger/Compat.hs +45/−5
- src/GHC/TypeLits/Presburger/Types.hs +29/−16
ghc-typelits-presburger.cabal view
@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.2.+-- This file has been generated from package.yaml by hpack version 0.33.0. -- -- see: https://github.com/sol/hpack ----- hash: 213617ccefa67bad574a0687988e14cef38a75e07ac2e08140bcda55feeee3f6+-- hash: 3e336ef49eb47a4a5b2a74bdb84e17585fa0870e8c22e48ebb8402904c01ffe7 name: ghc-typelits-presburger-version: 0.3.0.0+version: 0.3.0.1 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.@@ -29,7 +29,7 @@ copyright: 2015 (c) Hiromi ISHII license: BSD3 license-file: LICENSE-tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.2+tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.1 build-type: Simple source-repository head@@ -56,7 +56,7 @@ base >=4.7 && <5 , containers , ghc >=7.10 && <8.11- , ghc-tcplugins-extra >=0.2 && <0.4+ , ghc-tcplugins-extra >=0.2 && <0.5 , mtl , pretty , reflection
src/GHC/TypeLits/Presburger/Compat.hs view
@@ -5,11 +5,10 @@ import Data.Function (on) import FamInst as GHC.TypeLits.Presburger.Compat import FastString as GHC.TypeLits.Presburger.Compat (fsLit)+import Class import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName, tracePlugin)-import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..))-import GhcPlugins as GHC.TypeLits.Presburger.Compat (classifyPredType, isEqPred,- lookupTyCon, mkTyConTy)+import GhcPlugins as GHC.TypeLits.Presburger.Compat (lookupTyCon, mkTyConTy) import GhcPlugins as GHC.TypeLits.Presburger.Compat (mkTcOcc, ppr, promotedFalseDataCon) import GhcPlugins as GHC.TypeLits.Presburger.Compat (promotedTrueDataCon, text) import GhcPlugins as GHC.TypeLits.Presburger.Compat (tyConAppTyCon_maybe, typeKind)@@ -21,8 +20,8 @@ import TcHsType as GHC.TypeLits.Presburger.Compat (tcInferApps) import TcPluginM as GHC.TypeLits.Presburger.Compat (TcPluginM, tcLookupTyCon, tcPluginTrace)-import TcRnMonad as GHC.TypeLits.Presburger.Compat (Ct, TcPluginResult (..), isWanted)-import TcRnTypes as GHC.TypeLits.Presburger.Compat (TcPlugin (..), ctEvPred, ctEvidence)+import TcRnMonad as GHC.TypeLits.Presburger.Compat (TcPluginResult (..))+import TcRnTypes as GHC.TypeLits.Presburger.Compat (TcPlugin (..)) import TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts) import TcTypeNats as GHC.TypeLits.Presburger.Compat import TyCon as GHC.TypeLits.Presburger.Compat@@ -62,7 +61,35 @@ #if MIN_VERSION_ghc(8,8,1) import qualified TysWiredIn #endif+#if MIN_VERSION_ghc(8,8,1)+import TysWiredIn (eqTyConName)+#else+import PrelNames (eqTyConName)+#endif +#if MIN_VERSION_ghc(8,10,1)+import Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred(..))+import Predicate as GHC.TypeLits.Presburger.Compat (isEqPred)++import qualified Predicate as Old (classifyPredType)+import Predicate as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole)+import Constraint as GHC.TypeLits.Presburger.Compat + (Ct, ctEvidence, ctEvPred, isWanted)+#else+import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..))+import GhcPlugins as GHC.TypeLits.Presburger.Compat (isEqPred)+import qualified GhcPlugins as Old (classifyPredType)+import TcRnMonad as GHC.TypeLits.Presburger.Compat (Ct, isWanted)+import Type as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole)+import TcRnTypes as GHC.TypeLits.Presburger.Compat (ctEvPred, ctEvidence)+#endif+++#if MIN_VERSION_ghc(8,10,1)+type PredTree = Pred+#endif++ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 data TvSubst = TvSubst InScopeSet TvSubstEnv @@ -127,7 +154,11 @@ tcLookupTyCon =<< lookupOrig md (mkTcOcc ":~:") decompFunTy :: Type -> [Type]+#if MIN_VERSION_ghc(8,10,1)+decompFunTy (FunTy _ t1 t2) = t1 : decompFunTy t2+#else decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2+#endif decompFunTy t = [t] newtype TypeEq = TypeEq { runTypeEq :: Type }@@ -192,3 +223,12 @@ EqPred NomEq t u -> fromMaybe emptyTvSubst $ GHC.TypeLits.Presburger.Compat.tcUnifyTy t u _ -> emptyTvSubst #endif+++classifyPredType :: Type -> PredTree+classifyPredType ty = case Old.classifyPredType ty of+ e@EqPred{} -> e+ ClassPred cls [_,t1,t2]+ | className cls == eqTyConName+ -> EqPred NomEq t1 t2+ e -> e
src/GHC/TypeLits/Presburger/Types.hs view
@@ -11,6 +11,7 @@ import Class (classTyCon) import Control.Applicative ((<|>)) import Control.Arrow (second)+import Outputable (showSDocUnsafe) import Control.Monad (forM_, guard, mzero, unless) import Control.Monad.State.Class import Control.Monad.Trans.Class@@ -32,10 +33,16 @@ import PrelNames import TcPluginM (lookupOrig, newFlexiTyVar, newWanted, tcLookupClass)-import Type (mkPrimEqPredRole, mkTyVarTy)+import Type (mkTyVarTy) import TysWiredIn (promotedEQDataCon, promotedGTDataCon, promotedLTDataCon)+#if MIN_VERSION_ghc(8,8,1)+import TysWiredIn (eqTyConName)+#else+import PrelNames (eqTyConName)+#endif+ import Var #if MIN_VERSION_ghc(8,6,0) import Plugins (purePlugin)@@ -238,7 +245,7 @@ decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult decidePresburger _ genTrans _ gs [] [] = do- tcPluginTrace "Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs)+ tcPluginTrace "pres: Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs) trans <- genTrans give trans $ do ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred (deconsPred a)) gs@@ -258,10 +265,10 @@ give trans $ do gs' <- normaliseGivens gs let subst = mkSubstitution (gs' ++ ds)- tcPluginTrace "Current subst" (ppr subst)- tcPluginTrace "wanteds" $ ppr $ map deconsPred ws- tcPluginTrace "givens" $ ppr $ map (subsType subst . deconsPred) gs- tcPluginTrace "deriveds" $ ppr $ map deconsPred ds+ 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 <$> mapM@@ -279,15 +286,15 @@ | ct <- solved , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct) ]- tcPluginTrace "final premises" (text $ show prems0)- tcPluginTrace "final goals" (text $ show $ map snd wants)+ tcPluginTrace "pres: final premises" (text $ show prems0)+ tcPluginTrace "pres: final goals" (text $ show $ map snd wants) case testIf prems (foldr ((:&&) . snd) PTrue wants) of Proved -> do- tcPluginTrace "Proved" (text $ show $ map snd wants)- tcPluginTrace "... with coercions" (ppr coerced)+ tcPluginTrace "pres: Proved" (text $ show $ map snd wants)+ tcPluginTrace "pres: ... with coercions" (ppr coerced) return $ TcPluginOk coerced [] Disproved wit -> do- tcPluginTrace "Failed! " (text $ show wit)+ tcPluginTrace "pres: Failed! " (text $ show wit) return $ TcPluginContradiction $ map fst wants defaultTranslation :: TcPluginM Translation@@ -326,10 +333,10 @@ p <=> q = (p :&& q) :|| (Not p :&& Not q) withEv :: Ct -> (EvTerm, Ct)-withEv ct- | EqPred _ t1 t2 <- classifyPredType (deconsPred ct) =- (evByFiat "ghc-typelits-presburger" t1 t2, ct)- | otherwise = undefined+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 =@@ -349,6 +356,8 @@ , con `elem` trueData given = return PTrue | Just (con, []) <- splitTyConApp_maybe ty , con `elem` falseData given = return PFalse+ | cls@(EqPred NomEq _ _) <- classifyPredType ty+ = toPresburgerPredTree cls | isEqPred ty = toPresburgerPredTree $ classifyPredType ty | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r , con `elem` (tyEq given ++ tyEqBool given)@@ -378,7 +387,7 @@ , con `elem` natLeqBool given = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do- lift $ lift $ tcPluginTrace "EQBOOL:" $ ppr (p, q)+ lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q) (<=>) <$> toPresburgerPred p <*> toPresburgerPred q toPresburgerPredTree (EqPred NomEq n m) -- (n :: Nat) ~ (m :: Nat)@@ -462,7 +471,11 @@ simpleExp :: Given Translation => Type -> Type simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)+#if MIN_VERSION_ghc(8,10,1)+simpleExp (FunTy f t1 t2) = FunTy f (simpleExp t1) (simpleExp t2)+#else simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2)+#endif simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2) simpleExp (TyConApp tc (lastTwo -> ts)) = fromMaybe (TyConApp tc (map simpleExp ts)) $ asum (map simpler