ghc-typelits-presburger (empty) → 0.1.0.0
raw patch · 6 files changed
+453/−0 lines, 6 filesdep +basedep +equational-reasoningdep +ghcsetup-changed
Dependencies added: base, equational-reasoning, ghc, ghc-tcplugins-extra, ghc-typelits-presburger, presburger, reflection
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- examples/simple-arith.hs +35/−0
- ghc-typelits-presburger.cabal +48/−0
- src/GHC/Compat.hs +103/−0
- src/GHC/TypeLits/Presburger.hs +235/−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,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"
+ ghc-typelits-presburger.cabal view
@@ -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
+ src/GHC/Compat.hs view
@@ -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]
+ src/GHC/TypeLits/Presburger.hs view
@@ -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+