diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs --- a/examples/simple-arith.hs +++ b/examples/simple-arith.hs @@ -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 diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal --- a/ghc-typelits-presburger.cabal +++ b/ghc-typelits-presburger.cabal @@ -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. diff --git a/src/GHC/Compat.hs b/src/GHC/Compat.hs --- a/src/GHC/Compat.hs +++ b/src/GHC/Compat.hs @@ -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) diff --git a/src/GHC/TypeLits/Presburger.hs b/src/GHC/TypeLits/Presburger.hs --- a/src/GHC/TypeLits/Presburger.hs +++ b/src/GHC/TypeLits/Presburger.hs @@ -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