ghc-typelits-presburger 0.7.0.0 → 0.7.1.0
raw patch · 5 files changed
+89/−14 lines, 5 filesdep ~ghc-typelits-presburgerPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc-typelits-presburger
API changes (from Hackage documentation)
Files
- examples/simple-arith-core.hs +53/−2
- ghc-typelits-presburger.cabal +3/−3
- src/Data/Integer/SAT.hs +2/−5
- src/GHC/TypeLits/Presburger/Compat.hs +5/−0
- src/GHC/TypeLits/Presburger/Types.hs +26/−4
examples/simple-arith-core.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-}@@ -16,13 +17,18 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-} #endif module Main where +import Unsafe.Coerce import Data.Proxy+import Numeric.Natural import Data.Type.Equality import GHC.TypeLits+import Data.Void import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 import qualified Data.Type.Ord as DTO@@ -31,7 +37,6 @@ import Data.Type.Bool #endif - main :: IO () main = putStrLn "finished" @@ -109,9 +114,10 @@ (n <=? 2) :~: 'True rangeEqlLeq _ = Refl +data NProxy (n :: Nat) = NProxy+ -- GHC >= 9.2 only Tests #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902-data NProxy (n :: Nat) = NProxy ghc92NLeqToGt :: (n DTO.<=? m) ~ 'False => NProxy n -> NProxy m -> (n DTO.>? m) :~: 'True@@ -135,6 +141,12 @@ maxLeq :: n <= m => NProxy n -> NProxy m -> DTO.Max n m :~: m maxLeq _ _ = Refl++mkOrd :: forall n m. (n DTO.< m) => NProxy n -> NProxy m+mkOrd _ = NProxy++maxOrd :: forall n. (0 DTO.< n) => NProxy n+maxOrd = mkOrd (NProxy @(n - 1)) #endif #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904@@ -156,3 +168,42 @@ succGtZero :: NProxy n -> IsTrue (0 DTO.<? If (n == 0) (n + 1) n) succGtZero _ = Witness #endif++succStepBack :: (Succ n <= Succ m) => NProxy n -> NProxy m -> IsTrue (n <=? m)+succStepBack _ _ = Witness++type Succ n = n + 1++data Leq n m where+ ZeroLeq :: SNat m -> Leq 0 m+ SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1)++newtype SNat n = SNat Natural++data ZeroOrSucc n where+ IsZero :: ZeroOrSucc 0+ IsSucc ::+ SNat n ->+ ZeroOrSucc (n + 1)++viewNat :: forall n. SNat n -> ZeroOrSucc n+viewNat (SNat n) =+ if n == 0+ then unsafeCoerce IsZero+ else unsafeCoerce (SNat (n - 1))++pattern Zero :: forall n. () => n ~ 0 => SNat n+pattern Zero <- (viewNat -> IsZero)++pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n+pattern Succ n <- (viewNat -> IsSucc n)++{-# COMPLETE Zero, Succ #-}++succLeqZeroAbsurd :: SNat n -> IsTrue (Succ n <=? 0) -> Void+succLeqZeroAbsurd = undefined++boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m+boolToPropLeq Zero m = ZeroLeq m+boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m+boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness
ghc-typelits-presburger.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 5bdb1784549b51d4ed7b1ae34a734767d318511c03ce6a179548a7d14f66498a+-- hash: d6484409d9fcbd50b1fb2f56f79743a1587a1330768401bbaeecaa4e969e8160 name: ghc-typelits-presburger-version: 0.7.0.0+version: 0.7.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.@@ -75,7 +75,7 @@ build-depends: base , equational-reasoning- , ghc-typelits-presburger+ , ghc-typelits-presburger >=0.7.1.0 default-language: Haskell2010 if !(flag(examples)) buildable: False
src/Data/Integer/SAT.hs view
@@ -746,8 +746,6 @@ go None xs = xs instance Monad Answer where- return a = One a- #if !MIN_VERSION_ghc(8,8,1) fail _ = None #endif@@ -771,13 +769,12 @@ fmap f (Choice x1 x2) = Choice (fmap f x1) (fmap f x2) instance Applicative Answer where- pure = return+ pure = One (<*>) = ap newtype S a = S (RW -> Answer (a, RW)) instance Monad S where- return a = S $ \s -> return (a, s) S m >>= k = S $ \s -> do (a, s1) <- m s let S m1 = k a@@ -795,7 +792,7 @@ fmap = liftM instance Applicative S where- pure = return+ pure a = S $ \s -> pure (a, s) (<*>) = ap updS :: (RW -> (a, RW)) -> S a
src/GHC/TypeLits/Presburger/Compat.hs view
@@ -13,6 +13,11 @@ import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS) #if MIN_VERSION_ghc(9,4,1) import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..))+import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (cTupleTyCon, cTupleDataCon)+import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (evCast)+import GHC.Plugins as GHC.TypeLits.Presburger.Compat (mkUnivCo)+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (UnivCoProvenance(..))+import GHC.Core.DataCon as GHC.TypeLits.Presburger.Compat (dataConWrapId) #else import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..)) #endif
src/GHC/TypeLits/Presburger/Types.hs view
@@ -16,6 +16,8 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# OPTIONS_GHC -Wno-partial-type-signatures #-} -- | Since 0.3.0.0 module GHC.TypeLits.Presburger.Types ( pluginWith,@@ -40,6 +42,9 @@ import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName) import qualified Data.Integer.SAT as SAT import Data.List (nub)+#if MIN_VERSION_ghc(9,4,0)+import qualified GHC.Core as GHC (Expr(..))+#endif import qualified Data.List as L import qualified Data.Map.Strict as M import Data.Maybe@@ -51,7 +56,7 @@ ) import Data.Reflection (Given, give, given) import qualified Data.Set as Set-import GHC.TypeLits.Presburger.Compat+import GHC.TypeLits.Presburger.Compat as Compat import qualified Data.Foldable as F assert' :: Prop -> PropSet -> PropSet@@ -333,9 +338,9 @@ 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)+ [ (evProof, ct) | ct <- solved- , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)+ , Just evProof <- pure $ extractProof $ classifyPredType $ deconsPred ct ] tcPluginTrace "pres: final premises" (text $ show prems0) tcPluginTrace "pres: final goals" (text $ show $ map snd wants)@@ -348,6 +353,23 @@ tcPluginTrace "pres: Failed! " (text $ show wit) return $ TcPluginContradiction $ map fst wants ++extractProof :: Given Translation => PredTree -> Maybe EvTerm+extractProof (EqPred NomEq t1 t2) = + Just $ evByFiat "ghc-typelits-presburger" t1 t2+#if MIN_VERSION_base(4,17,0)+extractProof (IrredPred prd)+ | Just (con, lastN 2 -> [_, _]) <- splitTyConApp_maybe prd+ , con `elem` assertTy given = + Just $ GHC.Var (dataConWrapId $ cTupleDataCon 0) `evCast`+ mkUnivCo+ (PluginProv $ "ghc-typelits-presburger: extractProof")+ Representational+ (mkTyConTy (cTupleTyCon 0))+ prd+#endif+extractProof _ = Nothing+ eqReasoning :: FastString eqReasoning = fsLit "equational-reasoning" @@ -721,7 +743,7 @@ #else simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2) #endif-#endif+#endif simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2) simpleExp (TyConApp tc (lastTwo -> ts)) = fromMaybe (TyConApp tc (map simpleExp ts)) $