ghc-typelits-presburger 0.2.0.3 → 0.2.0.4
raw patch · 4 files changed
+92/−17 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- examples/simple-arith.hs +14/−6
- ghc-typelits-presburger.cabal +1/−1
- src/GHC/Compat.hs +3/−0
- src/GHC/TypeLits/Presburger.hs +74/−10
examples/simple-arith.hs view
@@ -1,19 +1,28 @@-{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts, EmptyCase #-}+{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables, CPP #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} module Main where import Data.Type.Equality-import GHC.TypeLits (Nat, type (<=), type (*), type (+), type (<=?), CmpNat)+import GHC.TypeLits (Nat, type (*), type (+), type (<=?), CmpNat) import Proof.Propositional (Empty(..)) import Proof.Propositional (IsTrue(Witness))-import Data.Singletons.Prelude hiding (type (<=))+import Data.Singletons.Prelude+import qualified Data.Singletons.Prelude as Sing import Data.Void type n <=! m = IsTrue (n <=? m) infix 4 <=! -natLeqZero :: ((n <=? 0) ~ 'True) => proxy n -> n :~: 0-natLeqZero _ = Refl+-- natLeqZero :: ((n <=? 0) ~ 'True) => proxy n -> n :~: 0+-- natLeqZero _ = Refl +#if MIN_VERSION_singletons(2,4,1)+natLeqZero' :: ((n <= 0) ~ 'True) => proxy n -> n :~: 0+#else+natLeqZero' :: ((n :<= 0) ~ 'True) => proxy n -> n :~: 0+#endif+natLeqZero' _ = Refl+ -- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m) -- n %:<=? m = case sCompare n m of -- SLT -> STrue@@ -51,7 +60,6 @@ -- succLEqLTSucc :: Sing m -> Compare 0 (m + 1) :~: 'LT -- succLEqLTSucc _ = Refl- -- succCompare :: Sing (n :: Nat) -> Sing m -> CmpNat n m :~: CmpNat (n + 1) (m + 1) -- succCompare _ _ = Refl
ghc-typelits-presburger.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-presburger-version: 0.2.0.3+version: 0.2.0.4 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.
src/GHC/Compat.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE CPP, PatternGuards, PatternSynonyms, ViewPatterns #-} module GHC.Compat (module GHC.Compat) where+import FamInst as GHC.Compat import FastString as GHC.Compat (fsLit) import GHC.TcPluginM.Extra as GHC.Compat (evByFiat, lookupModule, lookupName, tracePlugin)@@ -14,10 +15,12 @@ import OccName as GHC.Compat (emptyOccSet, mkInstTyTcOcc) import Plugins as GHC.Compat (Plugin (..), defaultPlugin) import TcEvidence as GHC.Compat (EvTerm)+import TcHsType as GHC.Compat (tcInferApps) import TcPluginM as GHC.Compat (TcPluginM, tcLookupTyCon, tcPluginTrace) import TcRnMonad as GHC.Compat (Ct, TcPluginResult (..), isWanted) import TcRnTypes as GHC.Compat (TcPlugin (..), ctEvPred, ctEvidence)+import TcType as GHC.Compat (tcTyFamInsts) import TcTypeNats as GHC.Compat #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 import GhcPlugins (InScopeSet, Outputable, emptyUFM)
src/GHC/TypeLits/Presburger.hs view
@@ -1,10 +1,12 @@-{-# LANGUAGE CPP, FlexibleContexts, MultiWayIf, OverloadedStrings #-}-{-# LANGUAGE PatternGuards, RankNTypes, RecordWildCards, TupleSections #-}+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, MultiWayIf #-}+{-# LANGUAGE OverloadedStrings, PatternGuards, RankNTypes, RecordWildCards #-}+{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wno-unused-imports #-} module GHC.TypeLits.Presburger (plugin) where import GHC.Compat import Class (classTyCon)+import Control.Monad (replicateM) import Data.Foldable (asum) import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert) import Data.Integer.SAT (checkSat, noProps, toName)@@ -12,7 +14,13 @@ import Data.List (nub) import Data.Maybe (fromMaybe, isNothing, mapMaybe) import Data.Reflection (Given, give, given)-import TcPluginM (lookupOrig, tcLookupClass)+import Debug.Trace+import GHC.TypeLits (Nat)+import Outputable (showSDocUnsafe)+import TcPluginM (getFamInstEnvs, lookupOrig, matchFam,+ newFlexiTyVar, tcLookupClass,+ unsafeTcPluginTcM)+import Type (mkTyVarTy, splitTyConApp) import TysWiredIn (promotedEQDataCon, promotedGTDataCon, promotedLTDataCon) @@ -67,14 +75,26 @@ type PresState = () -data MyEnv = MyEnv { emptyClsTyCon :: TyCon- , eqTyCon_ :: TyCon- , eqWitCon_ :: TyCon- , isTrueCon_ :: TyCon- , voidTyCon :: TyCon- , typeLeqBoolTyCon_ :: TyCon- , singCompareCon_ :: TyCon+data MyEnv = MyEnv { emptyClsTyCon :: TyCon+ , eqTyCon_ :: TyCon+ , eqWitCon_ :: TyCon+ , isTrueCon_ :: TyCon+ , voidTyCon :: TyCon+ , typeLeqBoolTyCon_ :: TyCon+ , singCompareCon_ :: TyCon+ , caseNameForSingLeq_ :: TyCon+ , caseNameForSingGeq_ :: TyCon+ , caseNameForSingLt_ :: TyCon+ , caseNameForSingGt_ :: TyCon }+caseNameForSingLeq :: Given MyEnv => TyCon+caseNameForSingLeq = caseNameForSingLeq_ given+caseNameForSingGeq :: Given MyEnv => TyCon+caseNameForSingGeq = caseNameForSingGeq_ given+caseNameForSingLt :: Given MyEnv => TyCon+caseNameForSingLt = caseNameForSingLt_ given+caseNameForSingGt :: Given MyEnv => TyCon+caseNameForSingGt = caseNameForSingGt_ given eqTyCon :: Given MyEnv => TyCon eqTyCon = eqTyCon_ given@@ -147,12 +167,32 @@ singletons <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons") #if MIN_VERSION_singletons(2,4,1) typeLeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "<=")+ typeLtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "<")+ typeGeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ">=")+ typeGtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ">") #else typeLeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":<=")+ typeLtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":<")+ typeGeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":>=")+ typeGtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":>") #endif+ caseNameForSingLeq_ <- getCaseNameForSingletonOp typeLeqBoolTyCon_+ caseNameForSingLt_ <- getCaseNameForSingletonOp typeLtBoolTyCon_+ caseNameForSingGeq_ <- getCaseNameForSingletonOp typeGeqBoolTyCon_+ caseNameForSingGt_ <- getCaseNameForSingletonOp typeGtBoolTyCon_ singCompareCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "Compare") give MyEnv{..} act +getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon+getCaseNameForSingletonOp con = do+ let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]+ Just (appTy0, [n,b,bdy,r]) <- fmap (splitTyConApp . snd) <$> matchFam con vars+ let (appTy, args) = splitTyConApp bdy+ Just innermost <- fmap snd <$> matchFam appTy args+ Just (_, dat) <- matchFam appTy0 [n,b,innermost,r]+ Just dat' <- fmap snd <$> uncurry matchFam (splitTyConApp dat)+ return $ fst $ splitTyConApp dat'+ (<=>) :: Prop -> Prop -> Prop p <=> q = (p :&& q) :|| (Not p :&& Not q) @@ -199,6 +239,30 @@ | Just promotedTrueDataCon == tyConAppTyCon_maybe (substTy subst b) , Just (con, [t1, t2]) <- splitTyConApp_maybe (substTy subst p) , con `elem` boolLeqs = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2+ | Just promotedTrueDataCon == tyConAppTyCon_maybe (substTy subst b) -- Singleton's <=...+ , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p+ , con == caseNameForSingLeq+ , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singCompareCon, typeNatCmpTyCon] =+ (:<=) <$> toPresburgerExp subst l <*> toPresburgerExp subst r+ | Just promotedTrueDataCon == tyConAppTyCon_maybe (substTy subst b) -- Singleton's <...+ , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p+ , con == caseNameForSingLt+ , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singCompareCon, typeNatCmpTyCon] =+ (:<) <$> toPresburgerExp subst l <*> toPresburgerExp subst r+ | Just promotedTrueDataCon == tyConAppTyCon_maybe (substTy subst b) -- Singleton's >=...+ , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p+ , con == caseNameForSingGeq+ , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singCompareCon, typeNatCmpTyCon] =+ (:>=) <$> toPresburgerExp subst l <*> toPresburgerExp subst r+ | Just promotedTrueDataCon == tyConAppTyCon_maybe (substTy subst b) -- Singleton's >=...+ , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p+ , con == caseNameForSingGt+ , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singCompareCon, typeNatCmpTyCon] =+ (:>) <$> toPresburgerExp subst l <*> toPresburgerExp subst r toPresburgerPredTree subst (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) | typeKind p `eqType` mkTyConTy promotedBoolTyCon = (<=>) <$> toPresburgerPred subst p