ghc-typelits-presburger 0.1.1.0 → 0.1.1.1
raw patch · 4 files changed
+77/−66 lines, 4 filesdep +singletonsdep ~basedep ~equational-reasoningdep ~ghcPVP ok
version bump matches the API change (PVP)
Dependencies added: singletons
Dependency ranges changed: base, equational-reasoning, ghc, ghc-typelits-presburger, reflection
API changes (from Hackage documentation)
Files
- examples/simple-arith.hs +5/−3
- ghc-typelits-presburger.cabal +49/−46
- src/GHC/Compat.hs +5/−2
- src/GHC/TypeLits/Presburger.hs +18/−15
examples/simple-arith.hs view
@@ -1,17 +1,19 @@-{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-}+{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts, EmptyCase #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}+{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-} module Main where import Data.Type.Equality import GHC.TypeLits (Nat, type (<=), type (*), type (+), type (<=?), CmpNat) import Proof.Propositional (Empty(..)) import Proof.Propositional (IsTrue(Witness)) import Data.Singletons.Prelude+import Data.Void type n <=! m = IsTrue (n <=? m) infix 4 <=! --- natLeqZero :: (n <= 0) => proxy n -> n :~: 0--- natLeqZero _ = Refl+natLeqZero :: (n <= 0) => proxy n -> n :~: 0+natLeqZero _ = Refl -- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m) -- n %:<=? m = case sCompare n m of
ghc-typelits-presburger.cabal view
@@ -1,53 +1,56 @@-name: ghc-typelits-presburger-version: 0.1.1.0-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.- You can use by adding this package to @build-depends@ and add the following pragma to the head of .hs files:- .- > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger- -homepage: https://github.com/konn/ghc-typelits-presburger#readme-license: BSD3-license-file: LICENSE-author: Hiromi ISHII-maintainer: konn.jinro _at_ gmail.com-copyright: 2015 (c) Hiromi ISHII-category: Math, Type System-build-type: Simple--- extra-source-files:-cabal-version: >=1.10-tested-with: GHC == 7.10.3, GHC == 8.0.1+name: ghc-typelits-presburger+version: 0.1.1.1+cabal-version: >=1.10+build-type: Simple+license: BSD3+license-file: LICENSE+copyright: 2015 (c) Hiromi ISHII+maintainer: konn.jinro _at_ gmail.com+homepage: https://github.com/konn/ghc-typelits-presburger#readme+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.+ You can use by adding this package to @build-depends@ and add the following pragma to the head of .hs files:+ .+ > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger+category: Math, Type System+author: Hiromi ISHII+tested-with: GHC ==8.0.2 GHC ==8.2.2 +source-repository head+ type: git+ location: https://github.com/konn/ghc-typelits-presburger+ flag examples- Default: False+ default: False library- ghc-options: -Wall- hs-source-dirs: src- exposed-modules: GHC.TypeLits.Presburger- other-modules: GHC.Compat- build-depends: base >= 4.7 && < 5- , ghc >= 7.10 && < 8.2- , ghc-tcplugins-extra >= 0.2 && < 0.3- , presburger >= 1.3 && < 1.4- , equational-reasoning >= 0.4.0.0- , reflection- default-language: Haskell2010+ exposed-modules:+ GHC.TypeLits.Presburger+ build-depends:+ base >=4.7 && <5,+ ghc >=7.10 && <8.4,+ ghc-tcplugins-extra ==0.2.*,+ presburger ==1.3.*,+ equational-reasoning >=0.4.0.0 && <0.6,+ reflection >=2.1.2 && <2.2+ default-language: Haskell2010+ hs-source-dirs: src+ other-modules:+ GHC.Compat+ ghc-options: -Wall executable simple-arith- if flag(examples)- buildable: True- else- buildable: False- hs-source-dirs: examples- Main-is: simple-arith.hs- build-depends: base- , ghc-typelits-presburger- , equational-reasoning- default-language: Haskell2010- ghc-options: -Wall+ + if !flag(examples)+ buildable: False+ main-is: simple-arith.hs+ build-depends:+ base >=4.10.1.0 && <4.11,+ ghc-typelits-presburger >=0.1.1.1 && <0.2,+ equational-reasoning >=0.5.0.0 && <0.6,+ singletons >=2.3.1 && <2.4+ default-language: Haskell2010+ hs-source-dirs: examples+ ghc-options: -Wall -source-repository head- type: git- location: https://github.com/konn/ghc-typelits-presburger
src/GHC/Compat.hs view
@@ -38,7 +38,7 @@ import Unify as GHC.Compat (tcUnifyTy) #endif import TcPluginM (lookupOrig)-import Type as GHC.Compat (isVoidTy, splitTyConApp_maybe)+import Type as GHC.Compat (splitTyConApp_maybe) import Unique as GHC.Compat (getKey, getUnique) #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800@@ -71,9 +71,12 @@ | Old.isFunTy t = Just (t1, t2) viewFunTy _ = Nothing +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 802+#else pattern FunTy :: Type -> Type -> Type pattern FunTy t1 t2 <- (viewFunTy -> Just (t1, t2)) where FunTy t1 t2 = Old.mkFunTy t1 t2+#endif tcUnifyTy :: Type -> Type -> Maybe TvSubst tcUnifyTy t1 t2 = fromTCv <$> Old.tcUnifyTy t1 t2@@ -98,4 +101,4 @@ decompFunTy :: Type -> [Type] decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2-decompFunTy t = [t]+decompFunTy t = [t]
src/GHC/TypeLits/Presburger.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE FlexibleContexts, MultiWayIf, OverloadedStrings, PatternGuards #-}-{-# LANGUAGE RankNTypes, TupleSections, ViewPatterns #-}+{-# LANGUAGE RankNTypes, TupleSections #-} module GHC.TypeLits.Presburger (plugin) where import GHC.Compat @@ -9,7 +9,7 @@ import Data.Integer.SAT (assert, checkSat, noProps, toName) import qualified Data.Integer.SAT as SAT import Data.List (nub)-import Data.Maybe (fromMaybe, isNothing, mapMaybe)+import Data.Maybe (catMaybes, fromMaybe, isNothing, mapMaybe) import Data.Reflection (Given) import Data.Reflection (given) import Data.Reflection (give)@@ -28,7 +28,7 @@ isProved :: Proof -> Bool isProved Proved = True-isProved _ = False+isProved _ = False varsProp :: Prop -> [SAT.Name] varsProp (p :|| q) = nub $ varsProp p ++ varsProp q@@ -36,11 +36,11 @@ varsProp (Not p) = varsProp p varsProp (e :== v) = nub $ varsExpr e ++ varsExpr v varsProp (e :/= v) = nub $ varsExpr e ++ varsExpr v-varsProp (e :< v) = nub $ varsExpr e ++ varsExpr v-varsProp (e :> v) = nub $ varsExpr e ++ varsExpr v+varsProp (e :< v) = nub $ varsExpr e ++ varsExpr v+varsProp (e :> v) = nub $ varsExpr e ++ varsExpr v varsProp (e :<= v) = nub $ varsExpr e ++ varsExpr v varsProp (e :>= v) = nub $ varsExpr e ++ varsExpr v-varsProp _ = []+varsProp _ = [] varsExpr :: Expr -> [SAT.Name] varsExpr (e :+ v) = nub $ varsExpr e ++ varsExpr v@@ -73,6 +73,7 @@ , eqTyCon_ :: TyCon , eqWitCon_ :: TyCon , isTrueCon_ :: TyCon+ , voidTyCon :: TyCon } eqTyCon :: Given MyEnv => TyCon@@ -102,6 +103,7 @@ | Proved <- testIf prem p = (ct : ss, prem) | otherwise = (ss, assert' p prem) decidePresburger _ref gs ds ws = withTyCons $ do+ tcPluginTrace "Env" $ ppr (emptyTyCon, eqTyCon, eqWitnessTyCon, isTrueTyCon) let subst = foldr unionTvSubst emptyTvSubst $ map genSubst (gs ++ ds) tcPluginTrace "Current subst" (ppr subst) tcPluginTrace "wanteds" $ ppr $ map (deconsPred) ws@@ -116,7 +118,7 @@ | ct <- solved , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct) ]- tcPluginTrace "prems" (text $ show prems)+ tcPluginTrace "prems" (text $ show $ map (toPresburgerPred subst .substTy subst . deconsPred) (gs ++ ds)) tcPluginTrace "final goals" (text $ show $ map snd wants) case testIf prems (foldr (:&&) PTrue (map snd wants)) of Proved -> do@@ -133,16 +135,22 @@ eqcon <- getEqTyCon witcon <- getEqWitnessTyCon pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")- trucon <- (tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue"))- give (MyEnv emptyCon eqcon witcon trucon) act+ trucon <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")+ vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")+ voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")+ give (MyEnv emptyCon eqcon witcon trucon voidTyCon) act +isVoidTy :: Given MyEnv => Type -> Bool+isVoidTy typ =+ tyConAppTyCon_maybe typ == Just (voidTyCon given)+ (<=>) :: Prop -> Prop -> Prop p <=> q = (p :&& q) :|| (Not p :&& Not q) genSubst :: Ct -> TvSubst genSubst ct = case classifyPredType (deconsPred ct) of EqPred NomEq t u -> fromMaybe emptyTvSubst $ tcUnifyTy t u- _ -> emptyTvSubst+ _ -> emptyTvSubst withEv :: Ct -> (EvTerm, Ct) withEv ct@@ -169,11 +177,6 @@ , con == emptyTyCon = Not <$> toPresburgerPred subst l | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l => , con == isTrueTyCon = toPresburgerPred subst l- | ts <- decompFunTy ty -- v -> v' -> ... -> Void- , (args , [vd]) <- splitAt (length ts - 1) ts- , isVoidTy vd = do- preds <- mapM (toPresburgerPred subst) args- return $ Not $ foldr (:&&) PTrue preds | otherwise = Nothing toPresburgerPredTree :: Given MyEnv => TvSubst -> PredTree -> Maybe Prop