diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs --- a/examples/simple-arith.hs +++ b/examples/simple-arith.hs @@ -1,16 +1,25 @@ -{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeApplications #-} -{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators #-} -{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-} -{-# OPTIONS_GHC -dcore-lint #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-} #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810 {-# LANGUAGE StandaloneKindSignatures #-} #endif +{-# OPTIONS_GHC -dcore-lint #-} +{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-} module Main where + import Data.Singletons.Decide import Data.Singletons.Prelude import Data.Singletons.Prelude.Enum @@ -18,9 +27,8 @@ import Data.Singletons.TH import Data.Singletons.TypeLits import Data.Type.Equality -import GHC.TypeLits (type (<=?), CmpNat, Nat) -import Proof.Propositional (Empty (..), withEmpty) -import Proof.Propositional (IsTrue (Witness)) +import GHC.TypeLits (CmpNat, Nat, type (<=?)) +import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) #if !MIN_VERSION_singletons(2,4,0) import Data.Promotion.Prelude.Num @@ -35,14 +43,16 @@ #endif type n <=! m = IsTrue (n <=? m) + infix 4 <=! -natLen :: (Length xs <= Length ys) ~ 'True - => proxy xs -> proxy ys -> (Length ys - Length xs) + Length xs :~: Length ys +natLen :: + (Length xs <= Length ys) ~ 'True => + proxy xs -> + proxy ys -> + (Length ys - Length xs) + Length xs :~: Length ys natLen _ _ = Refl - --- The following three cases fails >= GHC 8.6. natLeqZero' :: ((n <= 0) ~ 'True) => proxy n -> n :~: 0 natLeqZero' _ = Refl @@ -59,7 +69,7 @@ viewNat :: Sing n -> NatView n viewNat sn = case sn %~ (sing :: Sing 0) of - Proved Refl -> IsZero + Proved Refl -> IsZero Disproved _emp -> withEmpty _emp $ IsSucc $ sPred sn plusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m) @@ -84,7 +94,7 @@ bar _ = () trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1) -trans _ _ Witness = Witness +trans _ _ Witness = Witness eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1)) eqv _ _ = Refl @@ -101,23 +111,42 @@ eqToRefl :: Sing (n :: Nat) -> Sing (m :: Nat) -> CmpNat n m :~: 'EQ -> n :~: m eqToRefl _n _m Refl = Refl -singletonsOnly [d| - flipOrdering :: Ordering -> Ordering - flipOrdering EQ = EQ - flipOrdering LT = GT - flipOrdering GT = LT - |] +minFlip :: (n <= m) ~ 'True => Proxy (m :: Nat) -> Proxy n -> Min m n :~: n +minFlip _ _ = Refl -flipCompare - :: forall n m. (KnownNat n, KnownNat m) - => Sing n -> Sing m -> FlipOrdering (Compare n m) :~: Compare m n -flipCompare n m = $(sCases ''Ordering [|sCompare n m|] [|Refl|]) +minMax :: (n <= m) ~ 'True => Proxy (m :: Nat) -> Proxy n -> Max m n :~: m +minMax _ _ = Refl -ltCompare - :: forall n m. (KnownNat n, KnownNat m, CmpNat n m ~ LT) - => Sing n -> Sing m -> Compare m n :~: GT +minComm :: Proxy (m :: Nat) -> Proxy n -> Min n m :~: Min m n +minComm _ _ = Refl + +maxComm :: Proxy (m :: Nat) -> Proxy n -> Max n m :~: Max m n +maxComm _ _ = Refl + +singletonsOnly + [d| + flipOrdering :: Ordering -> Ordering + flipOrdering EQ = EQ + flipOrdering LT = GT + flipOrdering GT = LT + |] + +flipCompare :: + forall n m. + (KnownNat n, KnownNat m) => + Sing n -> + Sing m -> + FlipOrdering (Compare n m) :~: Compare m n +flipCompare n m = + $(sCases ''Ordering [|sCompare n m|] [|Refl|]) + +ltCompare :: + forall n m. + (KnownNat n, KnownNat m, CmpNat n m ~ LT) => + Sing n -> + Sing m -> + Compare m n :~: GT ltCompare _ _ = Refl main :: IO () main = putStrLn "finished" - diff --git a/singletons-presburger.cabal b/singletons-presburger.cabal --- a/singletons-presburger.cabal +++ b/singletons-presburger.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 23033bfe49a2dac012b73e07213833c1ab32b4713b0a4cc1d4a4b772f8b74f5f +-- hash: 70dbe672ac6a08a171c823e902bc91918e2e99e85f85577e9d450133c8d5f202 name: singletons-presburger -version: 0.4.0.0 +version: 0.5.0.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. @@ -48,6 +48,7 @@ base >=4.7 && <5 , ghc >=7.10 && <8.11 , ghc-typelits-presburger >=0.4 + , mtl , reflection , singletons default-language: Haskell2010 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,61 +1,80 @@ -{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances #-} -{-# LANGUAGE MultiWayIf, OverloadedStrings, PatternGuards, RankNTypes #-} -{-# LANGUAGE RecordWildCards, TypeOperators, ViewPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} + module Data.Singletons.TypeNats.Presburger - (plugin, singletonTranslation - ) where -import GHC.TypeLits.Presburger.Compat -import GHC.TypeLits.Presburger.Types + ( plugin, + singletonTranslation, + ) +where import Control.Monad +import Control.Monad.Trans (MonadTrans (lift)) import Data.Reflection (Given, give, given) -import GHC (mkModule, moduleUnitId) -import TcPluginM (lookupOrig, matchFam) -import Type (splitTyConApp) +import GHC (mkModule, moduleUnitId) +import GHC.TypeLits.Presburger.Compat +import GHC.TypeLits.Presburger.Types +import TcPluginM (lookupOrig, matchFam) +import Type (splitTyConApp) plugin :: Plugin -plugin = pluginWith $ - (<>) <$> defaultTranslation <*> singletonTranslation +plugin = + pluginWith $ + (<>) <$> defaultTranslation <*> singletonTranslation -data SingletonCons - = SingletonCons - { singNatLeq :: TyCon - , singNatGeq :: TyCon - , singNatLt :: TyCon - , singNatGt :: TyCon - , singNatPlus :: TyCon - , singNatMinus :: TyCon - , singNatTimes :: TyCon - , singNatCompare :: TyCon - , singTrueSym0 :: TyCon - , singFalseSym0 :: TyCon - , caseNameForSingLeq :: TyCon - , caseNameForSingGeq :: TyCon - , caseNameForSingLt :: TyCon - , caseNameForSingGt :: TyCon - } +data SingletonCons = SingletonCons + { singNatLeq :: TyCon + , singNatGeq :: TyCon + , singNatLt :: TyCon + , singNatGt :: TyCon + , singNatPlus :: TyCon + , singNatMinus :: TyCon + , singNatTimes :: TyCon + , singNatCompare :: TyCon + , singTrueSym0 :: TyCon + , singFalseSym0 :: TyCon + , caseNameForSingLeq :: TyCon + , caseNameForSingGeq :: TyCon + , caseNameForSingLt :: TyCon + , caseNameForSingGt :: TyCon + , singMin :: TyCon + , singMax :: TyCon + , caseNameForMin :: TyCon + , caseNameForMax :: TyCon + } -singletonTranslation - :: TcPluginM Translation +singletonTranslation :: + TcPluginM Translation singletonTranslation = toTranslation <$> genSingletonCons -toTranslation - :: SingletonCons -> Translation -toTranslation scs@SingletonCons{..} = +toTranslation :: + SingletonCons -> Translation +toTranslation scs@SingletonCons {..} = give scs $ mempty - { natLeqBool = [singNatLeq] - , natGeqBool = [singNatGeq] - , natLtBool = [singNatLt] - , natGtBool = [singNatGt] - , natCompare = [singNatCompare] - , natPlus = [singNatPlus] - , natMinus = [singNatMinus] - , natTimes = [singNatTimes] - , parsePred = parseSingPred - , trueData = [singTrueSym0] - , falseData = [singFalseSym0] - } + { natLeqBool = [singNatLeq] + , natGeqBool = [singNatGeq] + , natLtBool = [singNatLt] + , natGtBool = [singNatGt] + , natCompare = [singNatCompare] + , natPlus = [singNatPlus] + , natMinus = [singNatMinus] + , natTimes = [singNatTimes] + , parsePred = parseSingPred + , parseExpr = parseSingExpr + , trueData = [singTrueSym0] + , natMin = [singMin] + , natMax = [singMax] + , falseData = [singFalseSym0] + } genSingletonCons :: TcPluginM SingletonCons genSingletonCons = do @@ -81,39 +100,81 @@ singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":*") singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":-") #endif - caseNameForSingLeq <- getCaseNameForSingletonOp singNatLeq - caseNameForSingLt <- getCaseNameForSingletonOp singNatLt - caseNameForSingGeq <- getCaseNameForSingletonOp singNatGeq - caseNameForSingGt <- getCaseNameForSingletonOp singNatGt + singMin <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Min") + singMax <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Max") + caseNameForSingLeq <- getCaseNameForSingletonBinRel singNatLeq + caseNameForSingLt <- getCaseNameForSingletonBinRel singNatLt + caseNameForSingGeq <- getCaseNameForSingletonBinRel singNatGeq + caseNameForSingGt <- getCaseNameForSingletonBinRel singNatGt + caseNameForMin <- getCaseNameForSingletonBinOp singMin + caseNameForMax <- getCaseNameForSingletonBinOp singMax singNatCompare <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Compare") - return SingletonCons{..} + tcPluginTrace "pres: minMaxes" $ + ppr (singMin, singMax, caseNameForMin, caseNameForMax) + return SingletonCons {..} -getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon -getCaseNameForSingletonOp con = do +getCaseNameForSingletonBinOp :: TyCon -> TcPluginM TyCon +getCaseNameForSingletonBinOp con = do let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)] tcPluginTrace "matching... for " (ppr con) - Just (appTy0, [n,b,bdy,r]) <- fmap (splitTyConApp . snd) <$> matchFam con vars + 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) <- matchFam appTy0 [n, b, innermost, r] Just dat' <- fmap snd <$> uncurry matchFam (splitTyConApp dat) + let Just (con', _) = splitTyConApp_maybe dat' + return con' + +getCaseNameForSingletonBinRel :: TyCon -> TcPluginM TyCon +getCaseNameForSingletonBinRel con = do + let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)] + tcPluginTrace "matching... for " (ppr con) + 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) tcPluginTrace "matched. (orig, inner) = " (ppr (con, fst $ splitTyConApp dat')) return $ fst $ splitTyConApp dat' lastTwo :: [a] -> [a] lastTwo = drop <$> subtract 2 . length <*> id -parseSingPred - :: (Given SingletonCons) - => (Type -> Machine Expr) -> Type -> Machine Prop +parseSingExpr :: + (Given SingletonCons) => + (Type -> Machine Expr) -> + Type -> + Machine Expr +parseSingExpr toE ty + | Just (con, [_, l, r, _]) <- splitTyConApp_maybe ty + , Just bin <- lookup 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 = + [ (caseNameForMin given, Min) + , (caseNameForMax given, Max) + ] + +parseSingPred :: + (Given SingletonCons) => + (Type -> Machine Expr) -> + Type -> + 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] = - bin <$> toExp l <*> toExp r - | otherwise = mzero + | Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe ty + , Just bin <- lookup con compCaseDic + , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy + , cmp `elem` [singNatCompare given, typeNatCmpTyCon] = + bin <$> toExp l <*> toExp r + | otherwise = do + lift $ lift $ tcPluginTrace "pres: Miokuring" (ppr ty) + mzero compCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)] compCaseDic = @@ -123,22 +184,22 @@ , (caseNameForSingGt given, (:>)) ] - -parseSingPredTree - :: Given SingletonCons - => (Type -> Machine Expr) - -> PredTree -> Machine Prop -parseSingPredTree toExp (EqPred NomEq p b) -- (n :<=? m) ~ 'True - | Just promotedTrueDataCon == tyConAppTyCon_maybe b -- Singleton's <=... - , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p - , Just bin <- lookup con compCaseDic - , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy - , cmp `elem` [singNatCompare given, typeNatCmpTyCon] = +parseSingPredTree :: + Given SingletonCons => + (Type -> Machine Expr) -> + PredTree -> + Machine Prop +parseSingPredTree toExp (EqPred NomEq p b) -- (n :<=? m) ~ 'True + | Just promotedTrueDataCon == tyConAppTyCon_maybe b -- Singleton's <=... + , Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe p + , Just bin <- lookup 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 (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy - , cmp `elem` [singNatCompare given, typeNatCmpTyCon] = + | Just promotedFalseDataCon == tyConAppTyCon_maybe b -- Singleton's <=... + , Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe p + , Just bin <- lookup con compCaseDic + , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy + , cmp `elem` [singNatCompare given, typeNatCmpTyCon] = fmap Not . bin <$> toExp l <*> toExp r parseSingPredTree _ _ = mzero