diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs new file mode 100644 --- /dev/null +++ b/examples/simple-arith.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} +module Main where +import Data.Type.Equality +import GHC.TypeLits (type (<=), type (*), type (+), type (<=?)) +import Proof.Propositional (Empty(..)) +import Proof.Propositional (IsTrue(Witness)) + +type n <=! m = IsTrue (n <=? m) +infix 4 <=! + +natLeqZero :: (n <= 0) => proxy n -> n :~: 0 +natLeqZero _ = Refl + + +hoge :: ((n + 1 <=? n) ~ 'False) => () +hoge = () + +fuga :: ((n + 1 <=? 0) ~ 'False) => () +fuga = () + +bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => () +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 + +main :: IO () +main = putStrLn "finished" diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal new file mode 100644 --- /dev/null +++ b/ghc-typelits-presburger.cabal @@ -0,0 +1,48 @@ +name: ghc-typelits-presburger +version: 0.1.0.0 +synopsis: Initial project template from stack +description: Please see README.md +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 + +flag examples + 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 + +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 + +source-repository head + type: git + location: https://github.com/konn/ghc-typelits-presburger diff --git a/src/GHC/Compat.hs b/src/GHC/Compat.hs new file mode 100644 --- /dev/null +++ b/src/GHC/Compat.hs @@ -0,0 +1,103 @@ +{-# LANGUAGE CPP, PatternGuards, PatternSynonyms, ViewPatterns #-} +module GHC.Compat (module GHC.Compat) where +import FastString as GHC.Compat (fsLit) +import GHC.TcPluginM.Extra as GHC.Compat (evByFiat, lookupModule, lookupName, + tracePlugin) +import GhcPlugins as GHC.Compat (EqRel (..), PredTree (..)) +import GhcPlugins as GHC.Compat (classifyPredType, isEqPred, + lookupTyCon, mkTyConTy) +import GhcPlugins as GHC.Compat (mkTcOcc, ppr, promotedFalseDataCon) +import GhcPlugins as GHC.Compat (promotedTrueDataCon, text) +import GhcPlugins as GHC.Compat (tyConAppTyCon_maybe, typeKind) +import GhcPlugins as GHC.Compat (TyCon, typeNatKind) +import Module as GHC.Compat (ModuleName, mkModuleName) +import Plugins as GHC.Compat (Plugin (..), defaultPlugin) +import TcEvidence as GHC.Compat (EvTerm) +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 TcTypeNats as GHC.Compat (typeNatAddTyCon, typeNatExpTyCon) +import TcTypeNats as GHC.Compat (typeNatLeqTyCon, typeNatMulTyCon) +import TcTypeNats as GHC.Compat (typeNatSubTyCon) +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 +import GhcPlugins (InScopeSet, Outputable, emptyUFM) +import qualified PrelNames as Old +import TyCoRep as GHC.Compat (TyLit (NumTyLit), Type (..)) +import Type as GHC.Compat (TCvSubst (..), TvSubstEnv, + emptyTCvSubst) +import Type as GHC.Compat (eqType, unionTCvSubst) +import qualified Type as Old +import qualified TysPrim as Old +import TysWiredIn as GHC.Compat (boolTyCon) +import Unify as Old (tcUnifyTy) +#else +import Type as GHC.Compat (TvSubst, emptyTvSubst) +import Type as GHC.Compat (substTy, unionTvSubst) +import TypeRep as GHC.Compat (TyLit (NumTyLit), Type (..)) +import TysWiredIn as Old (eqTyCon) +import TysWiredIn as GHC.Compat (promotedBoolTyCon) +import Unify as GHC.Compat (tcUnifyTy) +#endif +import TcPluginM (lookupOrig) +import Type as GHC.Compat (isVoidTy, splitTyConApp_maybe) +import Unique as GHC.Compat (getKey, getUnique) + +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 +data TvSubst = TvSubst InScopeSet TvSubstEnv + +instance Outputable TvSubst where + ppr = ppr . toTCv + +emptyTvSubst :: TvSubst +emptyTvSubst = case emptyTCvSubst of + TCvSubst set tvsenv _ -> TvSubst set tvsenv + +toTCv :: TvSubst -> TCvSubst +toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM + +substTy :: TvSubst -> Type -> Type +substTy tvs = Old.substTy (toTCv tvs) + +unionTvSubst :: TvSubst -> TvSubst -> TvSubst +unionTvSubst s1 s2 = + fromTCv $ unionTCvSubst (toTCv s1) (toTCv s2) +fromTCv :: TCvSubst -> TvSubst +fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv + +promotedBoolTyCon :: TyCon +promotedBoolTyCon = boolTyCon + +viewFunTy :: Type -> Maybe (Type, Type) +viewFunTy t@(TyConApp _ [t1, t2]) + | Old.isFunTy t = Just (t1, t2) +viewFunTy _ = Nothing + +pattern FunTy :: Type -> Type -> Type +pattern FunTy t1 t2 <- (viewFunTy -> Just (t1, t2)) where + FunTy t1 t2 = Old.mkFunTy t1 t2 + +tcUnifyTy :: Type -> Type -> Maybe TvSubst +tcUnifyTy t1 t2 = fromTCv <$> Old.tcUnifyTy t1 t2 + +getEqTyCon :: TcPluginM TyCon +getEqTyCon = tcLookupTyCon Old.eqTyConName + +#else +eqType :: Type -> Type -> Bool +eqType = (==) + +getEqTyCon :: TcPluginM TyCon +getEqTyCon = return Old.eqTyCon + +#endif + + +getEqWitnessTyCon :: TcPluginM TyCon +getEqWitnessTyCon = do + md <- lookupModule (mkModuleName "Data.Type.Equality") (fsLit "base") + tcLookupTyCon =<< lookupOrig md (mkTcOcc ":~:") + +decompFunTy :: Type -> [Type] +decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2 +decompFunTy t = [t] diff --git a/src/GHC/TypeLits/Presburger.hs b/src/GHC/TypeLits/Presburger.hs new file mode 100644 --- /dev/null +++ b/src/GHC/TypeLits/Presburger.hs @@ -0,0 +1,235 @@ +{-# LANGUAGE FlexibleContexts, MultiWayIf, OverloadedStrings, PatternGuards #-} +{-# LANGUAGE RankNTypes, TupleSections, ViewPatterns #-} +module GHC.TypeLits.Presburger (plugin) where +import GHC.Compat + +import Class (classTyCon) +import Data.Foldable (asum) +import Data.Integer.SAT (Expr (..), Prop (..), Prop, PropSet) +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.Reflection (Given) +import Data.Reflection (given) +import Data.Reflection (give) +import TcPluginM (tcLookupClass) +import TcPluginM (lookupOrig) + +assert' :: Prop -> PropSet -> PropSet +assert' p ps = foldr assert ps (p : varPos) + where + varPos = [K 0 :<= Var i | i <- varsProp p ] + +data Proof = Proved | Disproved [(Int, Integer)] + deriving (Read, Show, Eq, Ord) + +isProved :: Proof -> Bool +isProved Proved = True +isProved _ = False + +varsProp :: Prop -> [SAT.Name] +varsProp (p :|| q) = nub $ varsProp p ++ varsProp q +varsProp (p :&& q) = nub $ varsProp p ++ varsProp q +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 _ = [] + +varsExpr :: Expr -> [SAT.Name] +varsExpr (e :+ v) = nub $ varsExpr e ++ varsExpr v +varsExpr (e :- v) = nub $ varsExpr e ++ varsExpr v +varsExpr (_ :* v) = varsExpr v +varsExpr (Negate e) = varsExpr e +varsExpr (Var i) = [i] +varsExpr (K _) = [] +varsExpr (If p e v) = nub $ varsProp p ++ varsExpr e ++ varsExpr v +varsExpr (Div e _) = varsExpr e +varsExpr (Mod e _) = varsExpr e + +plugin :: Plugin +plugin = defaultPlugin { tcPlugin = const $ Just presburgerPlugin } + +presburgerPlugin :: TcPlugin +presburgerPlugin = + tracePlugin "typelits-presburger" $ + TcPlugin { tcPluginInit = return () -- tcPluginIO $ newIORef emptyTvSubst + , tcPluginSolve = decidePresburger + , tcPluginStop = const $ return () + } + +testIf :: PropSet -> Prop -> Proof +testIf ps q = maybe Proved Disproved $ checkSat (Not q `assert'` ps) + +type PresState = () + +data MyEnv = MyEnv { emptyClsTyCon :: TyCon + , eqTyCon_ :: TyCon + , eqWitCon_ :: TyCon + , isTrueCon_ :: TyCon + } + +eqTyCon :: Given MyEnv => TyCon +eqTyCon = eqTyCon_ given + +eqWitnessTyCon :: Given MyEnv => TyCon +eqWitnessTyCon = eqWitCon_ given + +isTrueTyCon :: Given MyEnv => TyCon +isTrueTyCon = isTrueCon_ given + +decidePresburger :: PresState -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult +decidePresburger _ref gs [] [] = do + tcPluginTrace "Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs) + withTyCons $ do + let subst = emptyTvSubst + -- foldr unionTvSubst emptyTvSubst $ map genSubst gs + givens = mapMaybe (\a -> (,) a <$> toPresburgerPred subst (deconsPred a)) gs + prems0 = map snd givens + prems = foldr assert' noProps prems0 + (solved, _) = foldr go ([], noProps) givens + if isNothing (checkSat prems) + then return $ TcPluginContradiction gs + else return $ TcPluginOk (map withEv solved) [] + where + go (ct, p) (ss, prem) + | Proved <- testIf prem p = (ct : ss, prem) + | otherwise = (ss, assert' p prem) +decidePresburger _ref gs ds ws = withTyCons $ do + let subst = foldr unionTvSubst emptyTvSubst $ map genSubst (gs ++ ds) + tcPluginTrace "Current subst" (ppr subst) + tcPluginTrace "wanteds" $ ppr $ map (deconsPred) ws + tcPluginTrace "givens" $ ppr $ map (deconsPred) gs + tcPluginTrace "deriveds" $ ppr $ map deconsPred ds + let wants = mapMaybe (\ct -> (,) ct <$> toPresburgerPred subst (substTy subst $ deconsPred ct)) $ + filter (isWanted . ctEvidence) ws + prems = foldr assert' noProps $ + mapMaybe (toPresburgerPred subst . substTy subst . deconsPred) (gs ++ ds) + solved = map fst $ filter (isProved . testIf prems . snd) wants + coerced = [(evByFiat "ghc-typelits-presburger" t1 t2, ct) + | ct <- solved + , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct) + ] + tcPluginTrace "prems" (text $ show prems) + tcPluginTrace "final goals" (text $ show $ map snd wants) + case testIf prems (foldr (:&&) PTrue (map snd wants)) of + Proved -> do + tcPluginTrace "Proved" (text $ show $ map snd wants) + return $ TcPluginOk coerced [] + Disproved wit -> do + tcPluginTrace "Failed! " (text $ show $ wit) + return $ TcPluginContradiction $ map fst wants + +withTyCons :: (Given MyEnv => TcPluginM a) -> TcPluginM a +withTyCons act = do + emd <- lookupModule (mkModuleName "Proof.Propositional.Empty") (fsLit "equational-reasoning") + emptyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty")) + 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 + +(<=>) :: 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 + +withEv :: Ct -> (EvTerm, Ct) +withEv ct + | EqPred _ t1 t2 <- classifyPredType (deconsPred ct) = + (evByFiat "ghc-typelits-presburger" t1 t2, ct) + | otherwise = undefined + +deconsPred :: Ct -> Type +deconsPred = ctEvPred . ctEvidence + +emptyTyCon :: Given MyEnv => TyCon +emptyTyCon = emptyClsTyCon given + +toPresburgerPred :: Given MyEnv => TvSubst -> Type -> Maybe Prop +toPresburgerPred subst (TyConApp con [t1, t2]) + | con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2 +toPresburgerPred subst ty + | isEqPred ty = toPresburgerPredTree subst $ classifyPredType ty + | Just (con, [l, r]) <- splitTyConApp_maybe ty + , con == eqTyCon = toPresburgerPredTree subst $ EqPred NomEq l r + | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty + , con == eqWitnessTyCon = toPresburgerPredTree subst $ EqPred NomEq l r + | Just (con, [l]) <- splitTyConApp_maybe ty + , con == emptyTyCon = Not <$> toPresburgerPred subst l + | Just (con, [l]) <- splitTyConApp_maybe ty + , con == isTrueTyCon = toPresburgerPred subst l + | ts <- decompFunTy ty + , (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 +toPresburgerPredTree subst (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True + | Just promotedFalseDataCon == tyConAppTyCon_maybe (substTy subst false) = + Not <$> toPresburgerPredTree subst (EqPred NomEq p (mkTyConTy promotedTrueDataCon)) +toPresburgerPredTree subst (EqPred NomEq p b) -- (n :<=? m) ~ 'True + | Just promotedTrueDataCon == tyConAppTyCon_maybe (substTy subst b) + , TyConApp con [t1, t2] <- substTy subst p + , con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2 +toPresburgerPredTree subst (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) + | typeKind p `eqType` mkTyConTy promotedBoolTyCon = + (<=>) <$> toPresburgerPred subst p + <*> toPresburgerPred subst q +toPresburgerPredTree subst (EqPred NomEq t1 t2) -- (n :: Nat) ~ (m :: Nat) + | typeKind t1 `eqType` typeNatKind = (:==) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2 +toPresburgerPredTree subst (ClassPred con [t1, t2]) -- (n :: Nat) ~ (m :: Nat) + | typeNatLeqTyCon == classTyCon con + , typeKind t1 `eqType` typeNatKind = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2 +toPresburgerPredTree _ _ = Nothing + +toPresburgerExp :: TvSubst -> Type -> Maybe Expr +toPresburgerExp dic ty = case substTy dic ty of + TyVarTy t -> Just $ Var $ toName $ getKey $ getUnique t + TyConApp tc ts -> + let step con op + | tc == con, [tl, tr] <- ts = + op <$> toPresburgerExp dic tl <*> toPresburgerExp dic tr + | otherwise = Nothing + in case ts of + [tl, tr] | tc == typeNatMulTyCon -> + case (simpleExp tl, simpleExp tr) of + (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> Just $ K $ n * m + (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp dic x + (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp dic x + _ -> Nothing + _ -> asum [ step con op + | (con, op) <- [(typeNatAddTyCon, (:+)), (typeNatSubTyCon, (:-))]] + LitTy (NumTyLit n) -> Just (K n) + _ -> Nothing + +simpleExp :: Type -> Type +simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2) +simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2) +simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2) +simpleExp (TyConApp tc ts) = fromMaybe (TyConApp tc (map simpleExp ts)) $ + asum (map simpler [(typeNatAddTyCon, (+)) + ,(typeNatSubTyCon, (-)) + ,(typeNatMulTyCon, (*)) + ,(typeNatExpTyCon, (^)) + ]) + where + simpler (con, op) + | con == tc, [tl, tr] <- map simpleExp ts = + Just $ + case (tl, tr) of + (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> LitTy (NumTyLit (op n m)) + _ -> TyConApp con [tl, tr] + | otherwise = Nothing +simpleExp t = t +