singletons-presburger 0.4.0.0 → 0.5.0.0
raw patch · 3 files changed
+201/−110 lines, 3 filesdep +mtlPVP ok
version bump matches the API change (PVP)
Dependencies added: mtl
API changes (from Hackage documentation)
Files
- examples/simple-arith.hs +57/−28
- singletons-presburger.cabal +3/−2
- src/Data/Singletons/TypeNats/Presburger.hs +141/−80
examples/simple-arith.hs view
@@ -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"-
singletons-presburger.cabal view
@@ -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 <https://hackage.haskell.org/package/singletons singletons> 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
src/Data/Singletons/TypeNats/Presburger.hs view
@@ -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