diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs --- a/examples/simple-arith-core.hs +++ b/examples/simple-arith-core.hs @@ -1,6 +1,15 @@ -{-# LANGUAGE CPP, DataKinds, EmptyCase, FlexibleContexts, GADTs, LambdaCase #-} -{-# LANGUAGE PolyKinds, ScopedTypeVariables, TypeFamilies, TypeInType #-} -{-# LANGUAGE TypeOperators, UndecidableInstances #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -dcore-lint #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} @@ -9,21 +18,25 @@ #endif module Main where + import Data.Proxy import Data.Type.Equality import GHC.TypeLits -import Proof.Propositional (Empty (..), withEmpty) -import Proof.Propositional (IsTrue (Witness)) +import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) type n <=! m = IsTrue (n <=? m) + infix 4 <=! type family Length (as :: [k]) where Length '[] = 0 Length (x ': xs) = 1 + Length xs -natLen :: (Length xs <= Length ys) - => proxy xs -> proxy ys -> (Length ys - Length xs) + Length xs :~: Length ys +natLen :: + (Length xs <= Length ys) => + proxy xs -> + proxy ys -> + (Length ys - Length xs) + Length xs :~: Length ys natLen _ _ = Refl natLeqZero' :: (n <= 0) => proxy n -> n :~: 0 @@ -35,15 +48,14 @@ leqEquiv :: (n <= m) => p n -> p m -> IsTrue (n <=? m) leqEquiv _ _ = Witness - plusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m) plusLeq _ _ = Refl minusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <=? m) minusLeq _ _ = Witness -absurdTrueFalse :: ('True :~: 'False) -> a -absurdTrueFalse = \case {} +absurdTrueFalse :: ( 'True :~: 'False) -> a +absurdTrueFalse = \case #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802 hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a @@ -56,16 +68,14 @@ barResult :: () barResult = bar (Proxy :: Proxy 2) - 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 predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n) predSucc _ = Witness - succLEqLTSucc :: pxy m -> CmpNat 0 (m + 1) :~: 'LT succLEqLTSucc _ = Refl diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal --- a/ghc-typelits-presburger.cabal +++ b/ghc-typelits-presburger.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 3e336ef49eb47a4a5b2a74bdb84e17585fa0870e8c22e48ebb8402904c01ffe7 +-- hash: c960b466954cc5f717d05e796b5bd46864fa0d34fe74e43583e277fb61613376 name: ghc-typelits-presburger -version: 0.3.0.1 +version: 0.4.0.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. @@ -29,7 +29,7 @@ copyright: 2015 (c) Hiromi ISHII license: BSD3 license-file: LICENSE -tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.1 +tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.3 build-type: Simple source-repository head @@ -77,4 +77,29 @@ , ghc-typelits-presburger if !(flag(examples)) buildable: False + default-language: Haskell2010 + +test-suite test-typeltis-presburger + type: exitcode-stdio-1.0 + main-is: test.hs + other-modules: + ErrorsNoPlugin + ErrorsWithPlugin + GHC.TypeLits.PresburgerSpec + Shared + Paths_ghc_typelits_presburger + hs-source-dirs: + test + ghc-options: -Wall -Wno-dodgy-imports + build-tool-depends: + tasty-discover:tasty-discover + build-depends: + base + , equational-reasoning + , ghc-typelits-presburger + , tasty + , tasty-discover + , tasty-expected-failure + , tasty-hunit + , text default-language: Haskell2010 diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs --- a/src/GHC/TypeLits/Presburger/Types.hs +++ b/src/GHC/TypeLits/Presburger/Types.hs @@ -1,49 +1,71 @@ -{-# LANGUAGE BangPatterns, CPP, DataKinds, FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances, LambdaCase, MultiWayIf, OverloadedStrings #-} -{-# LANGUAGE PatternGuards, RankNTypes, TypeOperators, ViewPatterns #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} + -- | Since 0.3.0.0 module GHC.TypeLits.Presburger.Types - ( pluginWith - , defaultTranslation - , Translation(..), ParseEnv, Machine - , module Data.Integer.SAT - ) where -import Class (classTyCon) -import Control.Applicative ((<|>)) -import Control.Arrow (second) -import Outputable (showSDocUnsafe) -import Control.Monad (forM_, guard, mzero, unless) -import Control.Monad.State.Class -import Control.Monad.Trans.Class -import Control.Monad.Trans.Maybe (MaybeT (..)) -import Control.Monad.Trans.RWS.Strict (runRWS, tell) -import Control.Monad.Trans.State (StateT, runStateT) -import Data.Foldable (asum) -import Data.Integer.SAT (Expr (..), Prop (..), PropSet, - assert) -import Data.Integer.SAT (checkSat, noProps, toName) -import qualified Data.Integer.SAT as SAT -import Data.List (nub) -import qualified Data.Map.Strict as M -import Data.Maybe (catMaybes, fromMaybe, - isNothing) -import Data.Reflection (Given, give, given) -import qualified Data.Set as Set -import GHC.TypeLits.Presburger.Compat -import PrelNames -import TcPluginM (lookupOrig, newFlexiTyVar, - newWanted, tcLookupClass) -import Type (mkTyVarTy) -import TysWiredIn (promotedEQDataCon, - promotedGTDataCon, - promotedLTDataCon) + ( pluginWith, + defaultTranslation, + Translation (..), + ParseEnv, + Machine, + module Data.Integer.SAT, + ) +where + +import Class (classTyCon) +import Control.Applicative ((<|>)) +import Control.Arrow (second) +import Control.Monad (forM_, guard, mzero, unless) +import Control.Monad.State.Class +import Control.Monad.Trans.Class +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Control.Monad.Trans.RWS.Strict (runRWS, tell) +import Control.Monad.Trans.State (StateT, runStateT) +import Data.Foldable (asum) +import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName) +import qualified Data.Integer.SAT as SAT +import Data.List (nub) +import qualified Data.Map.Strict as M +import Data.Maybe + ( catMaybes, + fromMaybe, + isNothing, + ) +import Data.Reflection (Given, give, given) +import qualified Data.Set as Set +import GHC.TypeLits.Presburger.Compat +import Outputable (showSDocUnsafe) +import PrelNames +import TcPluginM + ( lookupOrig, + newFlexiTyVar, + newWanted, + tcLookupClass, + ) +import Type (mkTyVarTy) +import TysWiredIn + ( promotedEQDataCon, + promotedGTDataCon, + promotedLTDataCon, + ) #if MIN_VERSION_ghc(8,8,1) import TysWiredIn (eqTyConName) #else import PrelNames (eqTyConName) #endif -import Var +import Var + #if MIN_VERSION_ghc(8,6,0) import Plugins (purePlugin) #endif @@ -51,44 +73,46 @@ assert' :: Prop -> PropSet -> PropSet assert' p ps = foldr assert ps (p : varPos) where - varPos = [K 0 :<= Var i | i <- varsProp p ] + varPos = [K 0 :<= Var i | i <- varsProp p] data Proof = Proved | Disproved [(Int, Integer)] - deriving (Read, Show, Eq, Ord) + deriving (Read, Show, Eq, Ord) isProved :: Proof -> Bool isProved Proved = True -isProved _ = False +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 (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 -varsExpr (e :- v) = nub $ varsExpr e ++ varsExpr v -varsExpr (_ :* v) = varsExpr v +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 (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 +varsExpr (Div e _) = varsExpr e +varsExpr (Mod e _) = varsExpr e -data PluginMode = DisallowNegatives - | AllowNegatives - deriving (Read, Show, Eq, Ord) +data PluginMode + = DisallowNegatives + | AllowNegatives + deriving (Read, Show, Eq, Ord) pluginWith :: TcPluginM Translation -> Plugin -pluginWith trans = defaultPlugin +pluginWith trans = + defaultPlugin { tcPlugin = Just . presburgerPlugin trans . procOpts #if MIN_VERSION_ghc(8,6,0) , pluginRecompile = purePlugin @@ -101,11 +125,13 @@ presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin presburgerPlugin trans mode = - tracePlugin "typelits-presburger" - TcPlugin { tcPluginInit = return () - , tcPluginSolve = decidePresburger mode trans - , tcPluginStop = const $ return () - } + tracePlugin + "typelits-presburger" + TcPlugin + { tcPluginInit = return () + , tcPluginSolve = decidePresburger mode trans + , tcPluginStop = const $ return () + } testIf :: PropSet -> Prop -> Proof testIf ps q = maybe Proved Disproved $ checkSat (Not q `assert'` ps) @@ -116,21 +142,20 @@ handleSubtraction AllowNegatives p = p handleSubtraction DisallowNegatives p0 = let (p, _, w) = runRWS (loop p0) () Set.empty - in foldr (:&&) p w + in foldr (:&&) p w where - loop PTrue = return PTrue - loop PFalse = return PFalse + loop PTrue = return PTrue + loop PFalse = return PFalse loop (q :|| r) = (:||) <$> loop q <*> loop r loop (q :&& r) = (:&&) <$> loop q <*> loop r - loop (Not q) = Not <$> loop q + loop (Not q) = Not <$> loop q loop (l :<= r) = (:<=) <$> loopExp l <*> loopExp r - loop (l :< r) = (:<) <$> loopExp l <*> loopExp r + loop (l :< r) = (:<) <$> loopExp l <*> loopExp r loop (l :>= r) = (:<=) <$> loopExp l <*> loopExp r - loop (l :> r) = (:>) <$> loopExp l <*> loopExp r + loop (l :> r) = (:>) <$> loopExp l <*> loopExp r loop (l :== r) = (:==) <$> loopExp l <*> loopExp r loop (l :/= r) = (:/=) <$> loopExp l <*> loopExp r - withPositive pos = do dic <- get unless (Set.member pos dic) $ do @@ -139,46 +164,45 @@ return pos loopExp e@(Negate _) = withPositive . Negate =<< loopExp e - loopExp (l :- r) = do + loopExp (l :- r) = do e <- (:-) <$> loopExp l <*> loopExp r withPositive e - loopExp (l :+ r) = (:+) <$> loopExp l <*> loopExp r - loopExp v@Var {} = return v + loopExp (l :+ r) = (:+) <$> loopExp l <*> loopExp r + loopExp v@Var {} = return v loopExp (c :* e) | c > 0 = (c :*) <$> loopExp e | otherwise = (negate c :*) <$> loopExp (Negate e) loopExp e@(K _) = return e -data Translation = - Translation - { isEmpty :: [TyCon] - , isTrue :: [TyCon] - , trueData :: [TyCon] - , falseData :: [TyCon] - , voids :: [TyCon] - , tyEq :: [TyCon] - , tyEqBool :: [TyCon] - , tyEqWitness :: [TyCon] - , tyNeqBool :: [TyCon] - , natPlus :: [TyCon] - , natMinus :: [TyCon] - , natExp :: [TyCon] - , natTimes :: [TyCon] - , natLeq :: [TyCon] - , natLeqBool :: [TyCon] - , natGeq :: [TyCon] - , natGeqBool :: [TyCon] - , natLt :: [TyCon] - , natLtBool :: [TyCon] - , natGt :: [TyCon] - , natGtBool :: [TyCon] - , orderingLT :: [TyCon] - , orderingGT :: [TyCon] - , orderingEQ :: [TyCon] - , natCompare :: [TyCon] - , parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop - , parseExpr :: Type -> Machine Expr - } +data Translation = Translation + { isEmpty :: [TyCon] + , isTrue :: [TyCon] + , trueData :: [TyCon] + , falseData :: [TyCon] + , voids :: [TyCon] + , tyEq :: [TyCon] + , tyEqBool :: [TyCon] + , tyEqWitness :: [TyCon] + , tyNeqBool :: [TyCon] + , natPlus :: [TyCon] + , natMinus :: [TyCon] + , natExp :: [TyCon] + , natTimes :: [TyCon] + , natLeq :: [TyCon] + , natLeqBool :: [TyCon] + , natGeq :: [TyCon] + , natGeqBool :: [TyCon] + , natLt :: [TyCon] + , natLtBool :: [TyCon] + , natGt :: [TyCon] + , natGtBool :: [TyCon] + , orderingLT :: [TyCon] + , orderingGT :: [TyCon] + , orderingEQ :: [TyCon] + , natCompare :: [TyCon] + , parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop + , parseExpr :: Type -> Machine Expr + } instance Semigroup Translation where l <> r = @@ -213,35 +237,36 @@ } instance Monoid Translation where - mempty = Translation - { isEmpty = mempty - , isTrue = mempty - , tyEq = mempty - , tyEqBool = mempty - , tyEqWitness = mempty - , tyNeqBool = mempty - , voids = mempty - , natPlus = mempty - , natMinus = mempty - , natTimes = mempty - , natExp = mempty - , natLeq = mempty - , natGeq = mempty - , natLt = mempty - , natGt = mempty - , natLeqBool = mempty - , natGeqBool = mempty - , natLtBool = mempty - , natGtBool = mempty - , orderingLT = mempty - , orderingGT = mempty - , orderingEQ = mempty - , natCompare = mempty - , trueData = [] - , falseData = [] - , parsePred = const $ const mzero - , parseExpr = const mzero - } + mempty = + Translation + { isEmpty = mempty + , isTrue = mempty + , tyEq = mempty + , tyEqBool = mempty + , tyEqWitness = mempty + , tyNeqBool = mempty + , voids = mempty + , natPlus = mempty + , natMinus = mempty + , natTimes = mempty + , natExp = mempty + , natLeq = mempty + , natGeq = mempty + , natLt = mempty + , natGt = mempty + , natLeqBool = mempty + , natGeqBool = mempty + , natLtBool = mempty + , natGtBool = mempty + , orderingLT = mempty + , orderingGT = mempty + , orderingEQ = mempty + , natCompare = mempty + , trueData = [] + , falseData = [] + , parsePred = const $ const mzero + , parseExpr = const mzero + } decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult decidePresburger _ genTrans _ gs [] [] = do @@ -251,41 +276,50 @@ ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred (deconsPred a)) gs let givens = catMaybes ngs prems0 = map snd givens - prems = foldr assert' noProps prems0 + 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 mode genTrans _ gs ds ws = do + where + go (ct, p) (ss, prem) + | Proved <- testIf prem p = (ct : ss, prem) + | otherwise = (ss, assert' p prem) +decidePresburger mode genTrans _ gs _ds ws = do trans <- genTrans give trans $ do gs' <- normaliseGivens gs - let subst = mkSubstitution (gs' ++ ds) + let subst = mkSubstitution gs' tcPluginTrace "pres: Current subst" (ppr subst) tcPluginTrace "pres: wanteds" $ ppr $ map (subsType subst . deconsPred . subsCt subst) ws tcPluginTrace "pres: givens" $ ppr $ map (subsType subst . deconsPred) gs - tcPluginTrace "pres: deriveds" $ ppr $ map deconsPred ds + tcPluginTrace "pres: deriveds" $ ppr $ map deconsPred _ds (prems, wants, prems0) <- do - wants <- catMaybes <$> - mapM - (\ct -> runMachine $ (,) ct <$> toPresburgerPred - ( subsType subst - $ deconsPred $ subsCt subst ct)) - (filter (isWanted . ctEvidence) ws) + wants <- + catMaybes + <$> mapM + ( \ct -> + runMachine $ + (,) ct + <$> toPresburgerPred + ( subsType subst $ + deconsPred $ subsCt subst ct + ) + ) + (filter (isWanted . ctEvidence) ws) - resls <- mapM (runMachine . toPresburgerPred . subsType subst . deconsPred) - (gs ++ ds) + resls <- + mapM + (runMachine . toPresburgerPred . subsType subst . deconsPred) + gs let prems = foldr assert' noProps $ catMaybes resls return (prems, map (second $ handleSubtraction mode) wants, catMaybes resls) let 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) - ] + coerced = + [ (evByFiat "ghc-typelits-presburger" t1 t2, ct) + | ct <- solved + , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct) + ] tcPluginTrace "pres: final premises" (text $ show prems0) tcPluginTrace "pres: final goals" (text $ show $ map snd wants) case testIf prems (foldr ((:&&) . snd) PTrue wants) of @@ -310,27 +344,27 @@ nLeq <- tcLookupTyCon =<< lookupOrig gHC_TYPENATS (mkTcOcc "<=") return mempty - { isEmpty = [emptyClsTyCon] - , tyEq = [eqTyCon_] - , tyEqWitness = [eqWitCon_] - , isTrue = [isTrueCon_] - , voids = [voidTyCon] - , natMinus = [typeNatSubTyCon] - , natPlus = [typeNatAddTyCon] - , natTimes = [typeNatMulTyCon] - , natExp = [typeNatExpTyCon] - , falseData = [promotedFalseDataCon] - , trueData = [promotedTrueDataCon] - , natLeqBool = [typeNatLeqTyCon] - , natLeq = [nLeq] - , natCompare = [typeNatCmpTyCon] - , orderingEQ = [promotedEQDataCon] - , orderingLT = [promotedLTDataCon] - , orderingGT = [promotedGTDataCon] - } + { isEmpty = [emptyClsTyCon] + , tyEq = [eqTyCon_] + , tyEqWitness = [eqWitCon_] + , isTrue = [isTrueCon_] + , voids = [voidTyCon] + , natMinus = [typeNatSubTyCon] + , natPlus = [typeNatAddTyCon] + , natTimes = [typeNatMulTyCon] + , natExp = [typeNatExpTyCon] + , falseData = [promotedFalseDataCon] + , trueData = [promotedTrueDataCon] + , natLeqBool = [typeNatLeqTyCon] + , natLeq = [nLeq] + , natCompare = [typeNatCmpTyCon] + , orderingEQ = [promotedEQDataCon] + , orderingLT = [promotedLTDataCon] + , orderingGT = [promotedGTDataCon] + } (<=>) :: Prop -> Prop -> Prop -p <=> q = (p :&& q) :|| (Not p :&& Not q) +p <=> q = (p :&& q) :|| (Not p :&& Not q) withEv :: Ct -> (EvTerm, Ct) withEv ct = @@ -340,34 +374,39 @@ orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)] orderingDic = - [(lt, (:<)) | lt <- orderingLT given ] ++ - [(eq, (:==)) | eq <- orderingEQ given ] ++ - [(gt, (:>)) | gt <- orderingGT given ] + [(lt, (:<)) | lt <- orderingLT given] + ++ [(eq, (:==)) | eq <- orderingEQ given] + ++ [(gt, (:>)) | gt <- orderingGT given] deconsPred :: Ct -> Type deconsPred = ctEvPred . ctEvidence toPresburgerPred :: Given Translation => Type -> Machine Prop toPresburgerPred (TyConApp con [t1, t2]) - | con `elem` (natLeq given ++ natLeqBool given) - = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 + | con `elem` (natLeq given ++ natLeqBool given) = + (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 toPresburgerPred ty | Just (con, []) <- splitTyConApp_maybe ty - , con `elem` trueData given = return PTrue + , con `elem` trueData given = + return PTrue | Just (con, []) <- splitTyConApp_maybe ty - , con `elem` falseData given = return PFalse - | cls@(EqPred NomEq _ _) <- classifyPredType ty - = toPresburgerPredTree cls + , con `elem` falseData given = + return PFalse + | cls@(EqPred NomEq _ _) <- classifyPredType ty = + toPresburgerPredTree cls | isEqPred ty = toPresburgerPredTree $ classifyPredType ty | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r - , con `elem` (tyEq given ++ tyEqBool given) - = toPresburgerPredTree $ EqPred NomEq l r + , con `elem` (tyEq given ++ tyEqBool given) = + toPresburgerPredTree $ EqPred NomEq l r | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r - , con `elem` tyEqWitness given = toPresburgerPredTree $ EqPred NomEq l r + , con `elem` tyEqWitness given = + toPresburgerPredTree $ EqPred NomEq l r | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ... - , con `elem` isEmpty given = Not <$> toPresburgerPred l + , con `elem` isEmpty given = + Not <$> toPresburgerPred l | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l => - , con `elem` isTrue given = toPresburgerPred l + , con `elem` isTrue given = + toPresburgerPred l | otherwise = parsePred given toPresburgerExp ty splitTyConAppLastBin :: Type -> Maybe (TyCon, [Type]) @@ -381,88 +420,92 @@ toPresburgerPredTree (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True | maybe False (`elem` falseData given) $ tyConAppTyCon_maybe false = Not <$> toPresburgerPredTree (EqPred NomEq p (mkTyConTy promotedTrueDataCon)) -toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'True +toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'True | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b - , Just (con, [t1, t2]) <- splitTyConAppLastBin p - , con `elem` natLeqBool given = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 -toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) - | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do - lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q) - (<=>) <$> toPresburgerPred p - <*> toPresburgerPred q -toPresburgerPredTree (EqPred NomEq n m) -- (n :: Nat) ~ (m :: Nat) + , Just (con, [t1, t2]) <- splitTyConAppLastBin p + , con `elem` natLeqBool given = + (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 +toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) + | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do + lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q) + (<=>) <$> toPresburgerPred p + <*> toPresburgerPred q +toPresburgerPredTree (EqPred NomEq n m) -- (n :: Nat) ~ (m :: Nat) | typeKind n `eqType` typeNatKind = (:==) <$> toPresburgerExp n - <*> toPresburgerExp m + <*> toPresburgerExp m toPresburgerPredTree (EqPred _ t1 t2) -- CmpNat a b ~ CmpNat c d - | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t1 - , Just (con', lastTwo -> [c, d]) <- splitTyConAppLastBin t2 - , con `elem` natCompare given, con' `elem` natCompare given - = (<=>) <$> ((:<) <$> toPresburgerExp a <*> toPresburgerExp b) - <*> ((:<) <$> toPresburgerExp c <*> toPresburgerExp d) + | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t1 + , Just (con', lastTwo -> [c, d]) <- splitTyConAppLastBin t2 + , con `elem` natCompare given + , con' `elem` natCompare given = + (<=>) <$> ((:<) <$> toPresburgerExp a <*> toPresburgerExp b) + <*> ((:<) <$> toPresburgerExp c <*> toPresburgerExp d) toPresburgerPredTree (EqPred NomEq t1 t2) -- CmpNat a b ~ x | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t1 - , con `elem` natCompare given - , Just cmp <- tyConAppTyCon_maybe t2 = + , con `elem` natCompare given + , Just cmp <- tyConAppTyCon_maybe t2 = MaybeT (return $ lookup cmp orderingDic) - <*> toPresburgerExp a - <*> toPresburgerExp b + <*> toPresburgerExp a + <*> toPresburgerExp b toPresburgerPredTree (EqPred NomEq t1 t2) -- x ~ CmpNat a b | Just (con, lastTwo -> [a, b]) <- splitTyConAppLastBin t2 - , con `elem` natCompare given - , Just cmp <- tyConAppTyCon_maybe t1 = + , con `elem` natCompare given + , Just cmp <- tyConAppTyCon_maybe t1 = MaybeT (return $ lookup cmp orderingDic) - <*> toPresburgerExp a - <*> toPresburgerExp b + <*> toPresburgerExp a + <*> toPresburgerExp b toPresburgerPredTree (ClassPred con ts) -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat) - | let n = length ts, n >= 2 - , [t1, t2] <- drop (n - 2) ts - , typeKind t1 `eqType` typeNatKind - , typeKind t2 `eqType` typeNatKind = + | let n = length ts + , n >= 2 + , [t1, t2] <- drop (n - 2) ts + , typeKind t1 `eqType` typeNatKind + , typeKind t2 `eqType` typeNatKind = let p = lookup (classTyCon con) binPropDic - in MaybeT (return p) <*> toPresburgerExp t1 <*> toPresburgerExp t2 + in MaybeT (return p) <*> toPresburgerExp t1 <*> toPresburgerExp t2 toPresburgerPredTree _ = mzero binPropDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)] binPropDic = - [ (n, (:<)) | n <- natLt given ++ natLtBool given ] ++ - [ (n, (:>)) | n <- natGt given ++ natGtBool given ] ++ - [ (n, (:<=)) | n <- natLeq given ++ natLeqBool given ] ++ - [ (n, (:>=)) | n <- natGeq given ++ natGeqBool given ] ++ - [ (n, (:==)) | n <- tyEq given ++ tyEqBool given ] ++ - [ (n, (:/=)) | n <- tyNeqBool given ] + [(n, (:<)) | n <- natLt given ++ natLtBool given] + ++ [(n, (:>)) | n <- natGt given ++ natGtBool given] + ++ [(n, (:<=)) | n <- natLeq given ++ natLeqBool given] + ++ [(n, (:>=)) | n <- natGeq given ++ natGeqBool given] + ++ [(n, (:==)) | n <- tyEq given ++ tyEqBool given] + ++ [(n, (:/=)) | n <- tyNeqBool given] toPresburgerExp :: Given Translation => Type -> Machine Expr toPresburgerExp ty = case ty of - TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t + TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t t@(TyConApp tc ts) -> body tc ts <|> Var . toName . getKey . getUnique <$> toVar t LitTy (NumTyLit n) -> return (K n) - LitTy _ -> mzero - t -> - parseExpr given ty - <|> Var . toName . getKey .getUnique <$> toVar t + LitTy _ -> mzero + t -> + parseExpr given ty + <|> Var . toName . getKey . getUnique <$> toVar t where body tc ts = let step con op - | tc == con, [tl, tr] <- lastTwo ts = + | tc == con + , [tl, tr] <- lastTwo ts = op <$> toPresburgerExp tl <*> toPresburgerExp tr | otherwise = mzero - in case ts of - [tl, tr] | tc `elem` natTimes given -> - case (simpleExp tl, simpleExp tr) of - (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m - (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp x - (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp x - _ -> mzero - _ -> asum - $ [ step con (:+) - | con <- natPlus given - ] ++ - [ step con (:-) - | con <- natMinus given - ] - + in case ts of + [tl, tr] | tc `elem` natTimes given -> + case (simpleExp tl, simpleExp tr) of + (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m + (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp x + (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp x + _ -> mzero + _ -> + asum $ + [ step con (:+) + | con <- natPlus given + ] + ++ [ step con (:-) + | con <- natMinus given + ] -- simplTypeCmp :: Type -> Type @@ -477,20 +520,23 @@ simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2) #endif simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2) -simpleExp (TyConApp tc (lastTwo -> ts)) = fromMaybe (TyConApp tc (map simpleExp ts)) $ - asum (map simpler - $ [(c, (+)) | c <- natPlus given] ++ - [(c, (-)) | c <- natMinus given] ++ - [(c, (*)) | c <- natTimes given] ++ - [(c, (^)) | c <- natExp given] +simpleExp (TyConApp tc (lastTwo -> ts)) = + fromMaybe (TyConApp tc (map simpleExp ts)) $ + asum + ( map simpler $ + [(c, (+)) | c <- natPlus given] + ++ [(c, (-)) | c <- natMinus given] + ++ [(c, (*)) | c <- natTimes given] + ++ [(c, (^)) | c <- natExp given] ) where simpler (con, op) - | con == tc, [tl, tr] <- map simpleExp ts = + | 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] + case (tl, tr) of + (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> LitTy (NumTyLit (op n m)) + _ -> TyConApp con [tl, tr] | otherwise = Nothing simpleExp t = t @@ -506,9 +552,10 @@ return ma toVar :: Type -> Machine TyVar -toVar ty = gets (M.lookup (TypeEq ty)) >>= \case - Just v -> return v - Nothing -> do - v <- lift $ lift $ newFlexiTyVar $ typeKind ty - modify $ M.insert (TypeEq ty) v - return v +toVar ty = + gets (M.lookup (TypeEq ty)) >>= \case + Just v -> return v + Nothing -> do + v <- lift $ lift $ newFlexiTyVar $ typeKind ty + modify $ M.insert (TypeEq ty) v + return v diff --git a/test/ErrorsNoPlugin.hs b/test/ErrorsNoPlugin.hs new file mode 100644 --- /dev/null +++ b/test/ErrorsNoPlugin.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -fdefer-type-errors #-} + +module ErrorsNoPlugin where + +import Shared + +zipMVec :: Vec n a -> Vec n b -> Vec n (a, b) +zipMVec Nil Nil = Nil +zipMVec zs@(a :- as) (b :- bs) = (a, b) :- zipMVec zs bs + +spin :: Vec n a -> Vec n a -> () +spin _ _ = () + +unSpin :: Vec n a -> () +unSpin Nil = () +unSpin zs@(_ :- ws) = spin zs ws diff --git a/test/ErrorsWithPlugin.hs b/test/ErrorsWithPlugin.hs new file mode 100644 --- /dev/null +++ b/test/ErrorsWithPlugin.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -fdefer-type-errors #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +module ErrorsWithPlugin where + +import Shared + +zipMVec :: Vec n a -> Vec n b -> Vec n (a, b) +zipMVec Nil Nil = Nil +zipMVec zs@(a :- as) (b :- bs) = (a, b) :- zipMVec zs bs + +spin :: Vec n a -> Vec n a -> () +spin _ _ = () + +unSpin :: Vec n a -> () +unSpin Nil = () +unSpin zs@(_ :- ws) = spin zs ws diff --git a/test/GHC/TypeLits/PresburgerSpec.hs b/test/GHC/TypeLits/PresburgerSpec.hs new file mode 100644 --- /dev/null +++ b/test/GHC/TypeLits/PresburgerSpec.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE OverloadedStrings #-} + +module GHC.TypeLits.PresburgerSpec where + +import Control.Exception (evaluate, try) +import Control.Exception.Base (TypeError (TypeError)) +import Control.Monad (void) +import qualified Data.Text as T +import qualified ErrorsNoPlugin as NoPlugin +import qualified ErrorsWithPlugin as Plugin +import Shared +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (assertFailure, testCase) + +test_recursiveContradiction :: TestTree +test_recursiveContradiction = + testGroup + "n ~ n + 1 in recursive call should be rejected as type error" + [ testCase "Without plugin" $ do + eith <- try $ void (evaluate $ NoPlugin.zipMVec (True :- Nil) (() :- Nil)) + case eith of + Left (TypeError msg) + | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" + `T.isInfixOf` T.pack msg -> + pure () + _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith + , testCase "With plugin" $ do + eith <- try $ void (evaluate $ Plugin.zipMVec (True :- Nil) (() :- Nil)) + case eith of + Left (TypeError msg) + | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n" + `T.isInfixOf` T.pack msg -> + pure () + _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith + ] + +test_nonrecursiveContradiction :: TestTree +test_nonrecursiveContradiction = + testGroup + "n ~ n + 1 in non-recursive call should be rejected as type error" + [ testCase "Without plugin" $ do + eith <- try $ void (evaluate $ NoPlugin.unSpin (True :- Nil)) + case eith of + Left (TypeError msg) + | "Could not deduce: n1 ~ n" + `T.isInfixOf` T.pack msg -> + pure () + _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith + , testCase "With plugin" $ do + eith <- try $ void (evaluate $ Plugin.unSpin (True :- Nil)) + case eith of + Left (TypeError msg) + | "Could not deduce: n1 ~ n" + `T.isInfixOf` T.pack msg -> + pure () + _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith + ] diff --git a/test/Shared.hs b/test/Shared.hs new file mode 100644 --- /dev/null +++ b/test/Shared.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +module Shared (Vec (..)) where + +import GHC.TypeNats (Nat, type (+)) + +data Vec (n :: Nat) a where + Nil :: Vec 0 a + (:-) :: a -> Vec n a -> Vec (n + 1) a + +infixr 9 :- diff --git a/test/test.hs b/test/test.hs new file mode 100644 --- /dev/null +++ b/test/test.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF tasty-discover #-}