singletons-presburger (empty) → 0.3.0.0
raw patch · 5 files changed
+359/−0 lines, 5 filesdep +basedep +equational-reasoningdep +ghcsetup-changed
Dependencies added: base, equational-reasoning, ghc, ghc-typelits-presburger, reflection, singletons, singletons-presburger
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- examples/simple-arith.hs +120/−0
- singletons-presburger.cabal +69/−0
- src/Data/Singletons/TypeNats/Presburger.hs +138/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Hiromi ISHII (c) 2016++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Hiromi ISHII nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/simple-arith.hs view
@@ -0,0 +1,120 @@+{-# 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 #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806+{-# LANGUAGE NoStarIsType #-}+#endif++module Main where+import Data.Singletons.Decide+import Data.Singletons.Prelude+import Data.Singletons.Prelude.Enum+import Data.Singletons.Prelude.List+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))++#if !MIN_VERSION_singletons(2,4,0)+import Data.Promotion.Prelude.Num++type l <= m = l :<= m+type l * m = l :* m+type l + m = l :+ m+type l - m = l :- m+infix 4 <=+infixl 6 +, -+infixl 7 *+#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 _ _ = Refl+++-- The following three cases fails >= GHC 8.6.+natLeqZero' :: ((n <= 0) ~ 'True) => proxy n -> n :~: 0+natLeqZero' _ = Refl++leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) <= m) -> CmpNat n m :~: 'LT+leqSucc _ _ Witness = Refl++leqEquiv :: (n <= m) ~ 'True => Sing n -> Sing m -> IsTrue (n <=? m)+leqEquiv _ _ = Witness++data NatView (n :: Nat) where+ IsZero :: NatView 0+ IsSucc :: Sing n -> NatView (n + 1)++viewNat :: Sing n -> NatView n+viewNat sn =+ case sn %~ (sing :: Sing 0) of+ Proved Refl -> IsZero+ Disproved _emp -> withEmpty _emp $ IsSucc $ sPred sn++plusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m)+plusLeq _ _ = Refl++minusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <= m)+minusLeq _ _ = Witness++(%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)+n %:<=? m = case sCompare n m of+ SLT -> STrue+ SEQ -> STrue+ SGT -> SFalse++hoge :: ((n + 1 <=? n) ~ 'False) => proxy n -> ()+hoge _ = ()++hoge' :: (((n + 1) <= n) ~ 'False) => proxy n -> ()+hoge' _ = ()++bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> ()+bar _ = ()++trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)+trans _ _ Witness = Witness++eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))+eqv _ _ = Refl++predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)+predSucc _ = Witness++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++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+ |]++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
@@ -0,0 +1,69 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 1398143e2ff5a7650c68eda0c0513d0db5b5ed760488ce49e28425fa4f97830c++name: singletons-presburger+version: 0.3.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.+ .+ You can use by adding this package to @dependencies@ and add the following pragma+ to the head of .hs files:+ .+ > OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger+category: Math, Type System+homepage: https://github.com/konn/ghc-typelits-presburger#readme+bug-reports: https://github.com/konn/ghc-typelits-presburger/issues+author: Hiromi ISHII+maintainer: konn.jinro _at_ gmail.com+copyright: 2015 (c) Hiromi ISHII+license: BSD3+license-file: LICENSE+tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.2+build-type: Simple++source-repository head+ type: git+ location: https://github.com/konn/ghc-typelits-presburger++flag examples+ description: Builds example+ manual: False+ default: False++library+ exposed-modules:+ Data.Singletons.TypeNats.Presburger+ other-modules:+ Paths_singletons_presburger+ hs-source-dirs:+ src+ ghc-options: -Wall -Wno-dodgy-imports+ build-depends:+ base >=4.7 && <5+ , ghc >=7.10 && <8.11+ , ghc-typelits-presburger+ , reflection+ , singletons+ default-language: Haskell2010++executable simple-arith+ main-is: simple-arith.hs+ other-modules:+ Paths_singletons_presburger+ hs-source-dirs:+ examples+ ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports+ build-depends:+ base+ , equational-reasoning+ , singletons+ , singletons-presburger+ if !(flag(examples))+ buildable: False+ default-language: Haskell2010
+ src/Data/Singletons/TypeNats/Presburger.hs view
@@ -0,0 +1,138 @@+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE MultiWayIf, OverloadedStrings, PatternGuards, RankNTypes #-}+{-# LANGUAGE RecordWildCards, TypeOperators, ViewPatterns #-}+module Data.Singletons.TypeNats.Presburger+ (plugin, singletonTranslation+ ) where+import GHC.TypeLits.Presburger.Compat+import GHC.TypeLits.Presburger.Types++import Control.Monad+import Data.Reflection (Given, give, given)+import TcPluginM (lookupOrig, matchFam)+import Type (splitTyConApp)++plugin :: Plugin+plugin = pluginWith $+ (<>) <$> defaultTranslation <*> singletonTranslation++data SingletonCons+ = SingletonCons+ { singNatLeq :: TyCon+ , singNatGeq :: TyCon+ , singNatLt :: TyCon+ , singNatGt :: TyCon+ , singNatPlus :: TyCon+ , singNatMinus :: TyCon+ , singNatTimes :: TyCon+ , singNatCompare :: TyCon+ , caseNameForSingLeq :: TyCon+ , caseNameForSingGeq :: TyCon+ , caseNameForSingLt :: TyCon+ , caseNameForSingGt :: TyCon+ }++singletonTranslation+ :: TcPluginM Translation+singletonTranslation = toTranslation <$> genSingletonCons++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+ }++genSingletonCons :: TcPluginM SingletonCons+genSingletonCons = do+ singletonOrd <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")+ singletonsNum <- lookupModule (mkModuleName "Data.Singletons.Prelude.Num") (fsLit "singletons")+ -- prel <- lookupModule (mkModuleName "Data.Singletons.Prelude") (fsLit "singletons")+ -- singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")+#if MIN_VERSION_singletons(2,4,1)+ singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<=")+ singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<")+ singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ">=")+ singNatGt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ">")+ singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "+")+ singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "*")+ singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "-")+#else+ singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<=")+ singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<")+ singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>=")+ singNatGt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>")+ singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":+")+ singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":*")+ singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":-")+#endif+ caseNameForSingLeq <- getCaseNameForSingletonOp singNatLeq+ caseNameForSingLt <- getCaseNameForSingletonOp singNatLt+ caseNameForSingGeq <- getCaseNameForSingletonOp singNatGeq+ caseNameForSingGt <- getCaseNameForSingletonOp singNatGt+ singNatCompare <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Compare")+ return SingletonCons{..}++getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon+getCaseNameForSingletonOp 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+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++compCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]+compCaseDic =+ [ (caseNameForSingLeq given, (:<=))+ , (caseNameForSingLt given, (:<))+ , (caseNameForSingGeq given, (:>=))+ , (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] =+ 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] =+ fmap Not . bin <$> toExp l <*> toExp r+parseSingPredTree _ _ = mzero