ghc-typelits-presburger 0.1.1.1 → 0.7.4.2
raw patch · 15 files changed
Files
- Changelog.md +54/−0
- examples/simple-arith-core.hs +206/−0
- examples/simple-arith.hs +0/−61
- ghc-typelits-presburger.cabal +105/−43
- src/Data/Integer/SAT.hs +1021/−0
- src/GHC/Compat.hs +0/−104
- src/GHC/TypeLits/Presburger.hs +8/−266
- src/GHC/TypeLits/Presburger/Compat.hs +549/−0
- src/GHC/TypeLits/Presburger/Flags.hs +31/−0
- src/GHC/TypeLits/Presburger/Types.hs +773/−0
- test/ErrorsNoPlugin.hs +18/−0
- test/ErrorsWithPlugin.hs +19/−0
- test/GHC/TypeLits/PresburgerSpec.hs +70/−0
- test/Shared.hs +14/−0
- test/test.hs +1/−0
+ Changelog.md view
@@ -0,0 +1,54 @@+# Changelog++## 0.7.4.0++* Supports GHC 9.10+* Drops GHC <9.2++## 0.7.3.0++* Supports GHC 9.8+* Drops support for GHC <9++## 0.7.2.0++* Supports GHC 9.6+* More robust `equational-reasoning` package detection logic.++## 0.7.1.0++* Proper Support of GHC 9.4 (Now can solve `Assert` properly)++## 0.7.0.0++* Support GHC 9.4+* The plugin can solve constraints involving type-level `Assert`, `Not`, `(&&)`, `(||)`, and/or `If` from new base.++## 0.6.2.0++* Support GHC 9.2.1+* Decoding in Min/Max expression in terms of OrdCond++## 0.6.0.0++* Stop discharging redundant constraints+* Support GHC 9.0.1+* Drop a support for GHC <8.6++## 0.4.0.0++* Fixes constraint solving (fixes #9); this may change the previous (unsound) behaviour, and hence it is breaking change.++## 0.3.0.1++* Supports GHC >= 8.10.++## 0.3.0.0++* Drops support for GHC < 8.4+* Entire overhaul.+* Adds `negated-numbers` option.+* Allows terms which includes uninterpreted terms (still much incomplete).+* Separates `singletons` support as `singletons-presburger` package.+* Provides an interface for extending solver with additional syntax constructs.+ See `GHC.TypeLits.Presburger.Types` module for more detail.
+ examples/simple-arith-core.hs view
@@ -0,0 +1,206 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoStarIsType #-}+{-# OPTIONS_GHC -dcore-lint #-}+{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}++module Main where++import Data.Proxy+import Data.Type.Equality+import Data.Void+import GHC.TypeLits hiding (SNat)+import Numeric.Natural+import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty)+import Unsafe.Coerce+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902+import qualified Data.Type.Ord as DTO+#endif+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904+import Data.Type.Bool+#endif++main :: IO ()+main = putStrLn "finished"++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 _ _ = Refl++natLeqZero' :: (n <= 0) => proxy n -> n :~: 0+natLeqZero' _ = Refl++leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) <=? m) -> CmpNat n m :~: 'LT+leqSucc _ _ Witness = Refl++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 {}++hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a+hoge _ Witness = absurdTrueFalse Refl++bar :: ((2 * (n + 1)) ~ (2 * n + 2)) => proxy n -> ()+bar _ = ()++barResult :: ()+barResult = bar (Proxy :: Proxy 2)++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++predSuccBool :: forall proxy n. ((n <=? 0) ~ 'False) => proxy n -> IsTrue (n + 1 <=? 2 * n)+predSuccBool _ = Witness++predSuccProp :: forall proxy n. (Empty (n <=! 0)) => proxy n -> IsTrue (n + 1 <=? 2 * n)+predSuccProp _ = Witness++succLEqLTSucc :: pxy m -> CmpNat 0 (m + 1) :~: 'LT+succLEqLTSucc _ = Refl++succCompare :: pxy n -> pxy m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)+succCompare _ _ = Refl++eqToRefl :: pxy n -> pxy m -> CmpNat n m :~: 'EQ -> n :~: m+eqToRefl _n _m Refl = Refl++rangeEql ::+ ((n == 0) ~ 'False) =>+ pxy n ->+ (1 <=? n) :~: 'True+rangeEql _ = Refl++rangeEqlLeq ::+ ((n == 3) ~ 'False, n <= 3) =>+ pxy n ->+ (n <=? 2) :~: 'True+rangeEqlLeq _ = Refl++data NProxy (n :: Nat) = NProxy++-- GHC >= 9.2 only Tests+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902++ghc92NLeqToGt :: (n DTO.<=? m) ~ 'False + => NProxy n -> NProxy m -> (n DTO.>? m) :~: 'True+ghc92NLeqToGt _ _ = Refl++ghc92GtToGeq :: (n DTO.> m)+ => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'True+ghc92GtToGeq _ _ = Refl++ghc92GeqEquivNLt :: NProxy n -> NProxy m -> (n DTO.>=? m) :~: ((n DTO.<? m) == 'False)+ghc92GeqEquivNLt _ _ = Refl++-- N.B. We can't replace with predicate style with GHC 9.2.1+-- by the bug in base-4.16.0.0+ghc92NLtToGeq :: (n DTO.<? m) ~ 'True+ => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'False+ghc92NLtToGeq _ _ = Refl++minLeq :: n <= m => NProxy n -> NProxy m -> DTO.Min n m :~: n+minLeq _ _ = Refl++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+leqGeqToEq :: NProxy n -> NProxy m -> IsTrue (n <=? m && m <=? n) -> n :~: m+leqGeqToEq _ _ Witness = Refl++leqTotal :: NProxy n -> NProxy m -> IsTrue (n <=? m || m <=? n)+leqTotal _ _ = Witness++zeroMinimal :: NProxy n -> (n DTO.<? 0) :~: 'False+zeroMinimal _ = Refl++zeroMinimal' :: NProxy n -> IsTrue (Not (n DTO.<? 0))+zeroMinimal' _ = Witness++caseZero :: NProxy n -> IsTrue (If (n DTO.<=? 0) (n == 0) (n DTO.>? 0))+caseZero _ = Witness++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
− examples/simple-arith.hs
@@ -1,61 +0,0 @@-{-# 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---- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)--- n %:<=? m = case sCompare n m of--- SLT -> STrue--- SEQ -> STrue--- SGT -> SFalse---- natLeqZero :: IsTrue (n <=? 0) -> Sing n -> n :~: 0--- natLeqZero Witness Zero = Refl----- hoge :: ((n + 1 <=? n) ~ 'False) => ()--- hoge = ()---- fuga :: ((n + 1 <=? 0) ~ 'False) => ()--- fuga = ()---- bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> ()--- 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---- leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) :<= m) -> CmpNat n m :~: 'LT--- leqSucc _ _ Witness = Refl----- predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)--- predSucc _ = Witness--main :: IO ()-main = putStrLn "finished"---- succLEqLTSucc :: Sing m -> Compare 0 (m + 1) :~: 'LT--- succLEqLTSucc _ = Refl----- succCompare :: Sing (n :: Nat) -> Sing m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)--- succCompare _ _ = Refl--eqToRefl :: Sing (n :: Nat) -> Sing (m :: Nat) -> CmpNat n m :~: 'EQ -> n :~: m-eqToRefl _n _m Refl = Refl
ghc-typelits-presburger.cabal view
@@ -1,56 +1,118 @@+cabal-version: 3.4 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+version: 0.7.4.2 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+ @ghc-typelits-presburger@ augments GHC type-system with Presburger+ Arithmetic Solver for Type-level natural numbers.+ This plugin only work with GHC builtin operations.+ To work with those of @singletons@ package, use @ghc-typelits-meta@ and/or @ghc-typelits-presburger@ instead.+ .+ Since 0.3.0.0, integration with <https://hackage.haskell.org/package/singletons singletons> package moves to <https://hackage.haskell.org/package/singletons-presburger singletons-presburger>.+ .+ 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+homepage: https://github.com/konn/ghc-typelits-presburger#readme+bug-reports: https://github.com/konn/ghc-typelits-presburger/issues author: Hiromi ISHII-tested-with: GHC ==8.0.2 GHC ==8.2.2+maintainer: konn.jinro _at_ gmail.com+copyright: 2015-2025 (c) Hiromi ISHII+license: BSD-3-Clause+license-file: LICENSE+build-type: Simple+tested-with:+ ghc ==9.6.7+ ghc ==9.8.4+ ghc ==9.10.2+ ghc ==9.12.2 +extra-source-files:+ Changelog.md+ source-repository head- type: git- location: https://github.com/konn/ghc-typelits-presburger+ type: git+ location: https://github.com/konn/ghc-typelits-presburger flag examples- default: False+ description: Builds example+ manual: False+ default: False +common defaults+ autogen-modules: Paths_ghc_typelits_presburger+ other-modules: Paths_ghc_typelits_presburger+ default-language: Haskell2010+ ghc-options:+ -Wall+ -Wcompat+ -Widentities+ -Wincomplete-record-updates+ -Wincomplete-uni-patterns+ -Wmissing-export-lists+ -Wmissing-home-modules+ -Wpartial-fields+ -Wredundant-constraints+ -Wunused-packages+ library- 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+ import: defaults+ hs-source-dirs: src+ exposed-modules:+ GHC.TypeLits.Presburger+ GHC.TypeLits.Presburger.Compat+ GHC.TypeLits.Presburger.Types -executable simple-arith- - 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+ other-modules:+ Data.Integer.SAT+ GHC.TypeLits.Presburger.Flags + build-depends:+ base >=4.7 && <5,+ containers,+ ghc <9.13,+ ghc-tcplugins-extra >=0.2 && <0.6,+ mtl,+ pretty,+ reflection,+ syb,+ transformers,++executable simple-arith-core+ import: defaults+ main-is: simple-arith-core.hs+ hs-source-dirs: examples+ build-depends:+ base,+ equational-reasoning,+ ghc-typelits-presburger,++ if !(flag(examples))+ buildable: False++test-suite test-typeltis-presburger+ import: defaults+ type: exitcode-stdio-1.0+ main-is: test.hs+ hs-source-dirs: test+ -- cabal-gild: discover test --exclude=test/test.hs+ other-modules:+ ErrorsNoPlugin+ ErrorsWithPlugin+ GHC.TypeLits.PresburgerSpec+ Shared++ build-tool-depends: tasty-discover:tasty-discover+ build-depends:+ base,+ equational-reasoning,+ ghc-typelits-presburger,+ tasty,+ tasty-discover,+ tasty-expected-failure,+ tasty-hunit,+ text,
+ src/Data/Integer/SAT.hs view
@@ -0,0 +1,1021 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE Safe #-}++{- |+This module implements a decision procedure for quantifier-free linear+arithmetic. The algorithm is based on the following paper:++ An Online Proof-Producing Decision Procedure for+ Mixed-Integer Linear Arithmetic+ by+ Sergey Berezin, Vijay Ganesh, and David L. Dill+-}+module Data.Integer.SAT (+ PropSet,+ noProps,+ checkSat,+ assert,+ Prop (..),+ Expr (..),+ BoundType (..),+ getExprBound,+ getExprRange,+ Name,+ toName,+ fromName,++ -- * Iterators+ allSolutions,+ slnCurrent,+ slnNextVal,+ slnNextVar,+ slnEnumerate,++ -- * Debug+ dotPropSet,+ sizePropSet,+ allInerts,+ ppInerts,++ -- * For QuickCheck+ iPickBounded,+ Bound (..),+ tConst,+) where++import Control.Applicative (Alternative (..), Applicative (..), (<$>))+import Control.Monad (MonadPlus (..), ap, guard, liftM)+import Data.List (partition)+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe (fromMaybe, mapMaybe, maybeToList)+import Text.PrettyPrint+import Prelude hiding ((<>))++infixr 2 :||++infixr 3 :&&++infix 4 :==, :/=, :<, :<=, :>, :>=++infixl 6 :+, :-++infixl 7 :*++--------------------------------------------------------------------------------+-- Solver interface++-- | A collection of propositions.+newtype PropSet = State (Answer RW)+ deriving (Show)++dotPropSet :: PropSet -> Doc+dotPropSet (State a) = dotAnswer (ppInerts . inerts) a++sizePropSet :: PropSet -> (Integer, Integer, Integer)+sizePropSet (State a) = answerSize a++-- | An empty collection of propositions.+noProps :: PropSet+noProps = State $ return initRW++-- | Add a new proposition to an existing collection.+assert :: Prop -> PropSet -> PropSet+assert p (State rws) = State $ fmap snd $ m =<< rws+ where+ S m = prop p++{- | Extract a model from a consistent set of propositions.+ Returns 'Nothing' if the assertions have no model.+ If a variable does not appear in the assignment, then it is 0 (?).+-}+checkSat :: PropSet -> Maybe [(Int, Integer)]+checkSat (State m) = go m+ where+ go None = mzero+ go (One rw) = return [(x, v) | (UserName x, v) <- iModel (inerts rw)]+ go (Choice m1 m2) = mplus (go m1) (go m2)++allInerts :: PropSet -> [Inerts]+allInerts (State m) = map inerts (toList m)++allSolutions :: PropSet -> [Solutions]+allSolutions = map startIter . allInerts++{- | Computes bounds on the expression that are compatible with the model.+ Returns `Nothing` if the bound is not known.+-}+getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer+getExprBound bt e (State s) =+ do+ let S m = expr e+ check (t, s1) = iTermBound bt t (inerts s1)+ bs <- mapM check $ toList $ s >>= m+ case bs of+ [] -> Nothing+ _ -> Just (maximum bs)++{- | Compute the range of possible values for an expression.+ Returns `Nothing` if the bound is not known.+-}+getExprRange :: Expr -> PropSet -> Maybe [Integer]+getExprRange e (State s) =+ do+ let S m = expr e+ check (t, s1) = do+ l <- iTermBound Lower t (inerts s1)+ u <- iTermBound Upper t (inerts s1)+ return (l, u)+ bs <- mapM check $ toList $ s >>= m+ case bs of+ [] -> Nothing+ _ ->+ let (ls, us) = unzip bs+ in Just [x | x <- [minimum ls .. maximum us]]++-- | The type of proposition.+data Prop+ = PTrue+ | PFalse+ | Prop :|| Prop+ | Prop :&& Prop+ | Not Prop+ | Expr :== Expr+ | Expr :/= Expr+ | Expr :< Expr+ | Expr :> Expr+ | Expr :<= Expr+ | Expr :>= Expr+ deriving (Read, Show, Ord, Eq)++{- | The type of integer expressions.+ Variable names must be non-negative.+-}+data Expr+ = -- | Addition+ Expr :+ Expr+ | -- | Subtraction+ Expr :- Expr+ | -- | Multiplication by a constant+ Integer :* Expr+ | -- | Negation+ Negate Expr+ | -- | Variable+ Var Name+ | -- | Constant+ K Integer+ | -- | A conditional expression+ If Prop Expr Expr+ | -- | Division, rounds down+ Div Expr Integer+ | -- | Non-negative remainder+ Mod Expr Integer+ | -- | Minimum of two arguments+ Min Expr Expr+ | -- | Maximum of two arguments+ Max Expr Expr+ deriving (Read, Show, Ord, Eq)++prop :: Prop -> S ()+prop PTrue = return ()+prop PFalse = mzero+prop (p1 :|| p2) = prop p1 `mplus` prop p2+prop (p1 :&& p2) = prop p1 >> prop p2+prop (Not p) = prop (neg p)+ where+ neg PTrue = PFalse+ neg PFalse = PTrue+ neg (p1 :&& p2) = neg p1 :|| neg p2+ neg (p1 :|| p2) = neg p1 :&& neg p2+ neg (Not q) = q+ neg (e1 :== e2) = e1 :/= e2+ neg (e1 :/= e2) = e1 :== e2+ neg (e1 :< e2) = e1 :>= e2+ neg (e1 :<= e2) = e1 :> e2+ neg (e1 :> e2) = e1 :<= e2+ neg (e1 :>= e2) = e1 :< e2+prop (e1 :== e2) = do+ t1 <- expr e1+ t2 <- expr e2+ solveIs0 (t1 |-| t2)+prop (e1 :/= e2) = do+ t1 <- expr e1+ t2 <- expr e2+ let t = t1 |-| t2+ solveIsNeg t `orElse` solveIsNeg (tNeg t)+prop (e1 :< e2) = do+ t1 <- expr e1+ t2 <- expr e2+ solveIsNeg (t1 |-| t2)+prop (e1 :<= e2) = do+ t1 <- expr e1+ t2 <- expr e2+ let t = t1 |-| t2 |-| tConst 1+ solveIsNeg t+prop (e1 :> e2) = prop (e2 :< e1)+prop (e1 :>= e2) = prop (e2 :<= e1)++expr :: Expr -> S Term+expr (e1 :+ e2) = (|+|) <$> expr e1 <*> expr e2+expr (e1 :- e2) = (|-|) <$> expr e1 <*> expr e2+expr (k :* e2) = (k |*|) <$> expr e2+expr (Negate e) = tNeg <$> expr e+expr (Var x) = pure (tVar x)+expr (K x) = pure (tConst x)+expr (Min a b) = expr (If (a :<= b) a b)+expr (Max a b) = expr (If (a :<= b) b a)+expr (If p e1 e2) = do+ x <- newVar+ prop (p :&& Var x :== e1 :|| Not p :&& Var x :== e2)+ return (tVar x)+expr (Div e k) = fmap fst $ exprDivMod e k+expr (Mod e k) = fmap snd $ exprDivMod e k++exprDivMod :: Expr -> Integer -> S (Term, Term)+exprDivMod e k =+ do+ guard (k /= 0) -- Always unsat+ q <- newVar+ r <- newVar+ let er = Var r+ prop (k :* Var q :+ er :== e :&& er :< K k :&& K 0 :<= er)+ return (tVar q, tVar r)++--------------------------------------------------------------------------------++data RW = RW+ { nameSource :: !Int+ , inerts :: Inerts+ }+ deriving (Show)++initRW :: RW+initRW = RW {nameSource = 0, inerts = iNone}++--------------------------------------------------------------------------------+-- Constraints and Bound on Variables++ctLt :: Term -> Term -> Term+ctLt t1 t2 = t1 |-| t2++ctEq :: Term -> Term -> Term+ctEq t1 t2 = t1 |-| t2++data Bound+ = -- | The integer is strictly positive+ Bound Integer Term+ deriving (Show)++data BoundType = Lower | Upper+ deriving (Show)++toCt :: BoundType -> Name -> Bound -> Term+toCt Lower x (Bound c t) = ctLt t (c |*| tVar x)+toCt Upper x (Bound c t) = ctLt (c |*| tVar x) t++--------------------------------------------------------------------------------+-- Inert set++-- | The inert contains the solver state on one possible path.+data Inerts = Inerts+ { bounds :: NameMap ([Bound], [Bound])+ -- ^ Known lower and upper bounds for variables.+ -- Each bound @(c,t)@ in the first list asserts that @t < c * x@+ -- Each bound @(c,t)@ in the second list asserts that @c * x < t@+ , solved :: NameMap Term+ -- ^ Definitions for resolved variables.+ -- These form an idempotent substitution.+ }+ deriving (Show)++ppInerts :: Inerts -> Doc+ppInerts is =+ vcat $+ [ppLower x b | (x, (ls, _)) <- bnds, b <- ls]+ ++ [ppUpper x b | (x, (_, us)) <- bnds, b <- us]+ ++ [ppEq e | e <- Map.toList (solved is)]+ where+ bnds = Map.toList (bounds is)++ ppT c x = ppTerm (c |*| tVar x)+ ppLower x (Bound c t) = ppTerm t <+> text "<" <+> ppT c x+ ppUpper x (Bound c t) = ppT c x <+> text "<" <+> ppTerm t+ ppEq (x, t) = ppName x <+> text "=" <+> ppTerm t++-- | An empty inert set.+iNone :: Inerts+iNone =+ Inerts+ { bounds = Map.empty+ , solved = Map.empty+ }++-- | Rewrite a term using the definitions from an inert set.+iApSubst :: Inerts -> Term -> Term+iApSubst i t = foldr apS t $ Map.toList $ solved i+ where+ apS (x, t1) t2 = tLet x t1 t2++{- | Add a definition. Upper and lower bound constraints that mention+ the variable are "kicked-out" so that they can be reinserted in the+ context of the new knowledge.++ * Assumes substitution has already been applied.++ * The kicked-out constraints are NOT rewritten, this happens+ when they get inserted in the work queue.+-}+iSolved :: Name -> Term -> Inerts -> ([Term], Inerts)+iSolved x t i =+ ( kickedOut+ , Inerts+ { bounds = otherBounds+ , solved = Map.insert x t $ Map.map (tLet x t) $ solved i+ }+ )+ where+ (kickedOut, otherBounds) =+ -- First, we eliminate all entries for `x`+ let (mb, mp1) = Map.updateLookupWithKey (\_ _ -> Nothing) x (bounds i)++ -- Next, we elminate all constraints that mentiond `x` in bounds+ mp2 = Map.mapWithKey extractBounds mp1+ in ( [ ct | (lbs, ubs) <- maybeToList mb, ct <- map (toCt Lower x) lbs ++ map (toCt Upper x) ubs+ ]+ ++ [ct | (_, cts) <- Map.elems mp2, ct <- cts]+ , fmap fst mp2+ )++ extractBounds y (lbs, ubs) =+ let (lbsStay, lbsKick) = partition stay lbs+ (ubsStay, ubsKick) = partition stay ubs+ in ( (lbsStay, ubsStay)+ , map (toCt Lower y) lbsKick+ ++ map (toCt Upper y) ubsKick+ )++ stay (Bound _ bnd) = not (tHasVar x bnd)++{- | Given some lower and upper bounds, find the interval the satisfies them.+ Note the upper and lower bounds are strict (i.e., < and >)+-}+boundInterval :: [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)+boundInterval lbs ubs =+ do+ ls <- mapM (normBound Lower) lbs+ us <- mapM (normBound Upper) ubs+ let lb = case ls of+ [] -> Nothing+ _ -> Just (maximum ls + 1)+ ub = case us of+ [] -> Nothing+ _ -> Just (minimum us - 1)+ case (lb, ub) of+ (Just l, Just u) -> guard (l <= u)+ _ -> return ()+ return (lb, ub)+ where+ normBound Lower (Bound c t) = do+ k <- isConst t+ return (div (k + c - 1) c)+ normBound Upper (Bound c t) = do+ k <- isConst t+ return (div k c)++data Solutions+ = Done+ | TopVar Name Integer (Maybe Integer) (Maybe Integer) Inerts+ | FixedVar Name Integer Solutions+ deriving (Show)++slnCurrent :: Solutions -> [(Int, Integer)]+slnCurrent s = [(x, v) | (UserName x, v) <- go s]+ where+ go Done = []+ go (TopVar x v _ _ is) = (x, v) : iModel (iLet x v is)+ go (FixedVar x v i) = (x, v) : go i++{- | Replace occurances of a variable with an integer.+ WARNING: The integer should be a valid value for the variable.+-}+iLet :: Name -> Integer -> Inerts -> Inerts+iLet x v is =+ Inerts+ { bounds = fmap updBs (bounds is)+ , solved = fmap (tLetNum x v) (solved is)+ }+ where+ updB (Bound c t) = Bound c (tLetNum x v t)+ updBs (ls, us) = (map updB ls, map updB us)++startIter :: Inerts -> Solutions+startIter is =+ case Map.maxViewWithKey (bounds is) of+ Nothing ->+ case Map.maxViewWithKey (solved is) of+ Nothing -> Done+ Just ((x, t), mp1) ->+ case [y | y <- tVarList t] of+ y : _ -> TopVar y 0 Nothing Nothing is+ [] ->+ let v = tConstPart t+ in TopVar x v (Just v) (Just v) $ is {solved = mp1}+ Just ((x, (lbs, ubs)), mp1) ->+ case [y | Bound _ t <- lbs ++ ubs, y <- tVarList t] of+ y : _ -> TopVar y 0 Nothing Nothing is+ [] -> case boundInterval lbs ubs of+ Nothing -> error "bug: cannot compute interval?"+ Just (lb, ub) ->+ let v = fromMaybe 0 (mplus lb ub)+ in TopVar x v lb ub $ is {bounds = mp1}++slnEnumerate :: Solutions -> [Solutions]+slnEnumerate s0 = go s0 []+ where+ go s k = case slnNextVar s of+ Nothing -> hor s k+ Just s1 -> go s1 $ case slnNextVal s of+ Nothing -> k+ Just s2 -> go s2 k++ hor s k =+ s+ : case slnNextVal s of+ Nothing -> k+ Just s1 -> hor s1 k++slnNextVal :: Solutions -> Maybe Solutions+slnNextVal Done = Nothing+slnNextVal (FixedVar x v i) = FixedVar x v `fmap` slnNextVal i+slnNextVal it@(TopVar _ _ lb _ _) =+ case lb of+ Just _ -> slnNextValWith (+ 1) it+ Nothing -> slnNextValWith (subtract 1) it++slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions+slnNextValWith _ Done = Nothing+slnNextValWith f (FixedVar x v i) = FixedVar x v `fmap` slnNextValWith f i+slnNextValWith f (TopVar x v lb ub is) =+ do+ let v1 = f v+ case lb of+ Just l -> guard (l <= v1)+ Nothing -> return ()+ case ub of+ Just u -> guard (v1 <= u)+ Nothing -> return ()+ return $ TopVar x v1 lb ub is++slnNextVar :: Solutions -> Maybe Solutions+slnNextVar Done = Nothing+slnNextVar (TopVar x v _ _ is) = Just $ FixedVar x v $ startIter $ iLet x v is+slnNextVar (FixedVar x v i) = FixedVar x v `fmap` slnNextVar i++-- Given a list of lower (resp. upper) bounds, compute the least (resp. largest)+-- value that satisfies them all.+iPickBounded :: BoundType -> [Bound] -> Maybe Integer+iPickBounded _ [] = Nothing+iPickBounded bt bs =+ do+ xs <- mapM (normBound bt) bs+ return $ case bt of+ Lower -> maximum xs+ Upper -> minimum xs+ where+ -- t < c*x+ -- <=> t+1 <= c*x+ -- <=> (t+1)/c <= x+ -- <=> ceil((t+1)/c) <= x+ -- <=> t `div` c + 1 <= x+ normBound Lower (Bound c t) = do+ k <- isConst t+ return (k `div` c + 1)+ -- c*x < t+ -- <=> c*x <= t-1+ -- <=> x <= (t-1)/c+ -- <=> x <= floor((t-1)/c)+ -- <=> x <= (t-1) `div` c+ normBound Upper (Bound c t) = do+ k <- isConst t+ return (div (k - 1) c)++{- | The largest (resp. least) upper (resp. lower) bound on a term+ that will satisfy the model+-}+iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer+iTermBound bt (T k xs) is = do+ ks <- mapM summand (Map.toList xs)+ return $ sum $ k : ks+ where+ summand (x, c) = fmap (c *) (iVarBound (newBt c) x is)+ newBt c =+ if c > 0+ then bt+ else case bt of+ Lower -> Upper+ Upper -> Lower++{- | The largest (resp. least) upper (resp. lower) bound on a variable+ that will satisfy the model.+-}+iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer+iVarBound bt x is+ | Just t <- Map.lookup x (solved is) = iTermBound bt t is+iVarBound bt x is =+ do+ both <- Map.lookup x (bounds is)+ case mapMaybe fromBound (chooseBounds both) of+ [] -> Nothing+ bs -> return (combineBounds bs)+ where+ fromBound (Bound c t) = fmap (scaleBound c) (iTermBound bt t is)++ combineBounds = case bt of+ Upper -> minimum+ Lower -> maximum++ chooseBounds = case bt of+ Upper -> snd+ Lower -> fst++ scaleBound c b = case bt of+ Upper -> div (b - 1) c+ Lower -> div b c + 1++iModel :: Inerts -> [(Name, Integer)]+iModel i = goBounds [] (bounds i)+ where+ goBounds su mp =+ case Map.maxViewWithKey mp of+ Nothing -> goEqs su $ Map.toList $ solved i+ Just ((x, (lbs0, ubs0)), mp1) ->+ let lbs = [Bound c (tLetNums su t) | Bound c t <- lbs0]+ ubs = [Bound c (tLetNums su t) | Bound c t <- ubs0]+ sln =+ fromMaybe 0 $+ mplus (iPickBounded Lower lbs) (iPickBounded Upper ubs)+ in goBounds ((x, sln) : su) mp1++ goEqs su [] = su+ goEqs su ((x, t) : more) =+ let t1 = tLetNums su t+ vs = tVarList t1+ su1 = [(v, 0) | v <- vs] ++ (x, tConstPart t1) : su+ in goEqs su1 more++--------------------------------------------------------------------------------+-- Solving constraints++solveIs0 :: Term -> S ()+solveIs0 t = solveIs0' =<< apSubst t++{- | Solve a constraint if the form @t = 0@.+ Assumes substitution has already been applied.+-}+solveIs0' :: Term -> S ()+solveIs0' t+ -- A == 0+ | Just a <- isConst t = guard (a == 0)+ -- A + B * x = 0+ | Just (a, b, x) <- tIsOneVar t =+ case divMod (-a) b of+ (q, 0) -> addDef x (tConst q)+ _ -> mzero+ -- x + S = 0+ -- -x + S = 0+ | Just (xc, x, s) <- tGetSimpleCoeff t =+ addDef x (if xc > 0 then tNeg s else s)+ -- A * S = 0+ | Just (_, s) <- tFactor t = solveIs0 s+ -- See Section 3.1 of paper for details.+ -- We obtain an equivalent formulation but with smaller coefficients.+ | Just (ak, xk, s) <- tLeastAbsCoeff t =+ do+ let m = abs ak + 1+ v <- newVar+ let sgn = signum ak+ soln =+ (negate sgn * m)+ |*| tVar v+ |+| tMapCoeff (\c -> sgn * modulus c m) s+ addDef xk soln++ let upd i = div (2 * i + m) (2 * m) + modulus i m+ solveIs0 (negate (abs ak) |*| tVar v |+| tMapCoeff upd s)+ | otherwise = error "solveIs0: unreachable"++modulus :: Integer -> Integer -> Integer+modulus a m = a - m * div (2 * a + m) (2 * m)++solveIsNeg :: Term -> S ()+solveIsNeg t = solveIsNeg' =<< apSubst t++{- | Solve a constraint of the form @t < 0@.+ Assumes that substitution has been applied+-}+solveIsNeg' :: Term -> S ()+solveIsNeg' t+ -- A < 0+ | Just a <- isConst t = guard (a < 0)+ -- A * S < 0+ | Just (_, s) <- tFactor t = solveIsNeg s+ -- See Section 5.1 of the paper+ | Just (xc, x, s) <- tLeastVar t =+ do+ ctrs <-+ if xc < 0+ then -- -XC*x + S < 0+ -- S < XC*x+ do+ ubs <- getBounds Upper x+ let b = negate xc+ beta = s+ addBound Lower x (Bound b beta)+ return [(a, alpha, b, beta) | Bound a alpha <- ubs]+ else -- XC*x + S < 0+ -- XC*x < -S+ do+ lbs <- getBounds Lower x+ let a = xc+ alpha = tNeg s+ addBound Upper x (Bound a alpha)+ return [(a, alpha, b, beta) | Bound b beta <- lbs]++ -- See Note [Shadows]+ mapM_+ ( \(a, alpha, b, beta) ->+ do+ let real = ctLt (a |*| beta) (b |*| alpha)+ dark = ctLt (tConst (a * b)) (b |*| alpha |-| a |*| beta)+ gray =+ [ ctEq (b |*| tVar x) (tConst i |+| beta)+ | i <- [1 .. b - 1]+ ]+ solveIsNeg real+ foldl orElse (solveIsNeg dark) (map solveIs0 gray)+ )+ ctrs+ | otherwise = error "solveIsNeg: unreachable"++orElse :: S () -> S () -> S ()+orElse x y = mplus x y++{- Note [Shadows]++ P: beta < b * x+ Q: a * x < alpha++real: a * beta < b * alpha++ beta < b * x -- from P+ a * beta < a * b * x -- (a *)+ a * beta < b * alpha -- comm. and Q++dark: b * alpha - a * beta > a * b++gray: b * x = beta + 1 \/+ b * x = beta + 2 \/+ ...+ b * x = beta + (b-1)++We stop at @b - 1@ because if:++> b * x >= beta + b+> a * b * x >= a * (beta + b) -- (a *)+> a * b * x >= a * beta + a * b -- distrib.+> b * alpha > a * beta + a * b -- comm. and Q+> b * alpha - a * beta > a * b -- subtract (a * beta)++which is covered by the dark shadow.+-}++--------------------------------------------------------------------------------+-- Monads++data Answer a = None | One a | Choice (Answer a) (Answer a)+ deriving (Show)++answerSize :: Answer a -> (Integer, Integer, Integer)+answerSize = go 0 0 0+ where+ go !n !o !c ans =+ case ans of+ None -> (n + 1, o, c)+ One _ -> (n, o + 1, c)+ Choice x y ->+ case go n o (c + 1) x of+ (n', o', c') -> go n' o' c' y++dotAnswer :: (a -> Doc) -> Answer a -> Doc+dotAnswer pp g0 = vcat [text "digraph {", nest 2 (fst $ go 0 g0), text "}"]+ where+ node x d =+ integer x+ <+> brackets (text "label=" <> text (show d))+ <> semi+ edge x y = integer x <+> text "->" <+> integer y++ go x None =+ let x' = x + 1+ in seq x' (node x "", x')+ go x (One a) =+ let x' = x + 1+ in seq x' (node x (show (pp a)), x')+ go x (Choice c1 c2) =+ let x' = x + 1+ (ls1, x1) = go x' c1+ (ls2, x2) = go x1 c2+ in seq+ x'+ ( vcat+ [ node x "|"+ , edge x x'+ , edge x x1+ , ls1+ , ls2+ ]+ , x2+ )++toList :: Answer a -> [a]+toList a = go a []+ where+ go (Choice xs ys) zs = go xs (go ys zs)+ go (One x) xs = x : xs+ go None xs = xs++instance Monad Answer where+ None >>= _ = None+ One a >>= k = k a+ Choice m1 m2 >>= k = mplus (m1 >>= k) (m2 >>= k)++instance Alternative Answer where+ empty = mzero+ (<|>) = mplus++instance MonadPlus Answer where+ mzero = None+ mplus None x = x+ -- mplus (Choice x y) z = mplus x (mplus y z)+ mplus x y = Choice x y++instance Functor Answer where+ fmap _ None = None+ fmap f (One x) = One (f x)+ fmap f (Choice x1 x2) = Choice (fmap f x1) (fmap f x2)++instance Applicative Answer where+ pure = One+ (<*>) = ap++newtype S a = S (RW -> Answer (a, RW))++instance Monad S where+ S m >>= k = S $ \s -> do+ (a, s1) <- m s+ let S m1 = k a+ m1 s1++instance Alternative S where+ empty = mzero+ (<|>) = mplus++instance MonadPlus S where+ mzero = S $ \_ -> mzero+ mplus (S m1) (S m2) = S $ \s -> mplus (m1 s) (m2 s)++instance Functor S where+ fmap = liftM++instance Applicative S where+ pure a = S $ \s -> pure (a, s)+ (<*>) = ap++updS :: (RW -> (a, RW)) -> S a+updS f = S $ \s -> return (f s)++updS_ :: (RW -> RW) -> S ()+updS_ f = updS $ \rw -> ((), f rw)++get :: (RW -> a) -> S a+get f = updS $ \rw -> (f rw, rw)++newVar :: S Name+newVar = updS $ \rw ->+ ( SysName (nameSource rw)+ , rw {nameSource = nameSource rw + 1}+ )++-- | Get lower ('fst'), or upper ('snd') bounds for a variable.+getBounds :: BoundType -> Name -> S [Bound]+getBounds f x = get $ \rw -> case Map.lookup x $ bounds $ inerts rw of+ Nothing -> []+ Just bs -> case f of+ Lower -> fst bs+ Upper -> snd bs++addBound :: BoundType -> Name -> Bound -> S ()+addBound bt x b = updS_ $ \rw ->+ let i = inerts rw+ entry = case bt of+ Lower -> ([b], [])+ Upper -> ([], [b])+ jn (newL, newU) (oldL, oldU) = (newL ++ oldL, newU ++ oldU)+ in rw {inerts = i {bounds = Map.insertWith jn x entry (bounds i)}}++{- | Add a new definition.+ Assumes substitution has already been applied+-}+addDef :: Name -> Term -> S ()+addDef x t =+ do+ newWork <- updS $ \rw ->+ let (newWork, newInerts) = iSolved x t (inerts rw)+ in (newWork, rw {inerts = newInerts})+ mapM_ solveIsNeg newWork++apSubst :: Term -> S Term+apSubst t =+ do+ i <- get inerts+ return (iApSubst i t)++--------------------------------------------------------------------------------++data Name = UserName !Int | SysName !Int+ deriving (Read, Show, Eq, Ord)++ppName :: Name -> Doc+ppName (UserName x) = text "u" <> int x+ppName (SysName x) = text "s" <> int x++toName :: Int -> Name+toName = UserName++fromName :: Name -> Maybe Int+fromName (UserName x) = Just x+fromName (SysName _) = Nothing++type NameMap = Map Name++{- | The type of terms. The integer is the constant part of the term,+ and the `Map` maps variables (represented by @Int@ to their coefficients).+ The term is a sum of its parts.+ INVARIANT: the `Map` does not map anything to 0.+-}+data Term = T !Integer (NameMap Integer)+ deriving (Eq, Ord)++infixl 6 |+|, |-|++infixr 7 |*|++-- | A constant term.+tConst :: Integer -> Term+tConst k = T k Map.empty++-- | Construct a term with a single variable.+tVar :: Name -> Term+tVar x = T 0 (Map.singleton x 1)++(|+|) :: Term -> Term -> Term+T n1 m1 |+| T n2 m2 =+ T (n1 + n2) $+ if Map.null m1+ then m2+ else+ if Map.null m2+ then m1+ else Map.filter (/= 0) $ Map.unionWith (+) m1 m2++(|*|) :: Integer -> Term -> Term+0 |*| _ = tConst 0+1 |*| t = t+k |*| T n m = T (k * n) (fmap (k *) m)++tNeg :: Term -> Term+tNeg t = (-1) |*| t++(|-|) :: Term -> Term -> Term+t1 |-| t2 = t1 |+| tNeg t2++-- | Replace a variable with a term.+tLet :: Name -> Term -> Term -> Term+tLet x t1 t2 =+ let (a, t) = tSplitVar x t2+ in a |*| t1 |+| t++-- | Replace a variable with a constant.+tLetNum :: Name -> Integer -> Term -> Term+tLetNum x k t =+ let (c, T n m) = tSplitVar x t+ in T (c * k + n) m++-- | Replace the given variables with constants.+tLetNums :: [(Name, Integer)] -> Term -> Term+tLetNums xs t = foldr (\(x, i) t1 -> tLetNum x i t1) t xs++instance Show Term where+ showsPrec c t = showsPrec c (show (ppTerm t))++ppTerm :: Term -> Doc+ppTerm (T k m) =+ case Map.toList m of+ [] -> integer k+ xs | k /= 0 -> hsep (integer k : map ppProd xs)+ x : xs -> hsep (ppFst x : map ppProd xs)+ where+ ppFst (x, 1) = ppName x+ ppFst (x, -1) = text "-" <> ppName x+ ppFst (x, n) = ppMul n x++ ppProd (x, 1) = text "+" <+> ppName x+ ppProd (x, -1) = text "-" <+> ppName x+ ppProd (x, n)+ | n > 0 = text "+" <+> ppMul n x+ | otherwise = text "-" <+> ppMul (abs n) x++ ppMul n x = integer n <+> text "*" <+> ppName x++{- | Remove a variable from the term, and return its coefficient.+ If the variable is not present in the term, the coefficient is 0.+-}+tSplitVar :: Name -> Term -> (Integer, Term)+tSplitVar x t@(T n m) =+ case Map.updateLookupWithKey (\_ _ -> Nothing) x m of+ (Nothing, _) -> (0, t)+ (Just k, m1) -> (k, T n m1)++-- | Does the term contain this varibale?+tHasVar :: Name -> Term -> Bool+tHasVar x (T _ m) = Map.member x m++-- | Is this terms just an integer.+isConst :: Term -> Maybe Integer+isConst (T n m)+ | Map.null m = Just n+ | otherwise = Nothing++tConstPart :: Term -> Integer+tConstPart (T n _) = n++-- | Returns: @Just (a, b, x)@ if the term is the form: @a + b * x@+tIsOneVar :: Term -> Maybe (Integer, Integer, Name)+tIsOneVar (T a m) = case Map.toList m of+ [(x, b)] -> Just (a, b, x)+ _ -> Nothing++{- | Spots terms that contain variables with unit coefficients+ (i.e., of the form @x + t@ or @t - x@).+ Returns (coeff, var, rest of term)+-}+tGetSimpleCoeff :: Term -> Maybe (Integer, Name, Term)+tGetSimpleCoeff (T a m) =+ do+ let (m1, m2) = Map.partition (\x -> x == 1 || x == -1) m+ ((x, xc), m3) <- Map.minViewWithKey m1+ return (xc, x, T a (Map.union m3 m2))++tVarList :: Term -> [Name]+tVarList (T _ m) = Map.keys m++{- | Try to factor-out a common consant (> 1) from a term.+ For example, @2 + 4x@ becomes @2 * (1 + 2x)@.+-}+tFactor :: Term -> Maybe (Integer, Term)+tFactor (T c m) =+ do+ d <- common (c : Map.elems m)+ return (d, T (div c d) (fmap (`div` d) m))+ where+ common :: [Integer] -> Maybe Integer+ common [] = Nothing+ common [x] = Just x+ common (x : y : zs) =+ case gcd x y of+ 1 -> Nothing+ n -> common (n : zs)++-- | Extract a variable with a coefficient whose absolute value is minimal.+tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)+tLeastAbsCoeff (T c m) = do+ (xc, x, m1) <- Map.foldrWithKey step Nothing m+ return (xc, x, T c m1)+ where+ step x xc Nothing = Just (xc, x, Map.delete x m)+ step x xc (Just (yc, _, _))+ | abs xc < abs yc = Just (xc, x, Map.delete x m)+ step _ _ it = it++-- | Extract the least variable from a term+tLeastVar :: Term -> Maybe (Integer, Name, Term)+tLeastVar (T c m) =+ do+ ((x, xc), m1) <- Map.minViewWithKey m+ return (xc, x, T c m1)++-- | Apply a function to all coefficients, including the constnat+tMapCoeff :: (Integer -> Integer) -> Term -> Term+tMapCoeff f (T c m) = T (f c) (fmap f m)
− src/GHC/Compat.hs
@@ -1,104 +0,0 @@-{-# 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-#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 (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--#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--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
@@ -1,270 +1,12 @@-{-# LANGUAGE FlexibleContexts, MultiWayIf, OverloadedStrings, PatternGuards #-}-{-# LANGUAGE RankNTypes, TupleSections #-}-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 (catMaybes, fromMaybe, isNothing, mapMaybe)-import Data.Reflection (Given)-import Data.Reflection (given)-import Data.Reflection (give)-import TcPluginM (tcLookupClass)-import TcPluginM (lookupOrig)-import TysWiredIn (promotedEQDataCon, promotedGTDataCon,- promotedLTDataCon)--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+{- | Provides a plain Presburger solver plugin for @'GHC.TypeNats.Nat'@. -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 _ = []+ For an interface for extension, see+ "GHC.TypeLits.Presburger.Types".+-}+module GHC.TypeLits.Presburger (plugin) where -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+import GHC.TypeLits.Presburger.Compat+import GHC.TypeLits.Presburger.Types 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- , voidTyCon :: 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- 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- tcPluginTrace "givens" $ ppr $ map (substTy subst . 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 $ 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- 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")- 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--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 -- l ~ r- , con == eqTyCon = toPresburgerPredTree subst $ EqPred NomEq l r- | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r- , con == eqWitnessTyCon = toPresburgerPredTree subst $ EqPred NomEq l r- | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ...- , con == emptyTyCon = Not <$> toPresburgerPred subst l- | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>- , con == isTrueTyCon = toPresburgerPred subst l- | 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)- , Just (con, [t1, t2]) <- splitTyConApp_maybe (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 n m) -- (n :: Nat) ~ (m :: Nat)- | typeKind n `eqType` typeNatKind =- (:==) <$> toPresburgerExp subst n- <*> toPresburgerExp subst m-toPresburgerPredTree subst (EqPred _ t1 t2) -- CmpNat a b ~ CmpNat c d- | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t1)- , Just (con', [c, d]) <- splitTyConApp_maybe (substTy subst t2)- , con == typeNatCmpTyCon, con' == typeNatCmpTyCon- = (<=>) <$> ((:<) <$> toPresburgerExp subst a <*> toPresburgerExp subst b)- <*> ((:<) <$> toPresburgerExp subst c <*> toPresburgerExp subst d)-toPresburgerPredTree subst (EqPred NomEq t1 t2) -- CmpNat a b ~ x- | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t1)- , con == typeNatCmpTyCon- , Just cmp <- tyConAppTyCon_maybe (substTy subst t2) =- let dic = [(promotedLTDataCon, (:<))- ,(promotedEQDataCon, (:==))- ,(promotedGTDataCon, (:>))- ]- in lookup cmp dic <*> toPresburgerExp subst a- <*> toPresburgerExp subst b-toPresburgerPredTree subst (EqPred NomEq t1 t2) -- x ~ CmpNat a b- | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t2)- , con == typeNatCmpTyCon- , Just cmp <- tyConAppTyCon_maybe (substTy subst t1) =- let dic = [(promotedLTDataCon, (:<))- ,(promotedEQDataCon, (:==))- ,(promotedGTDataCon, (:>))- ]- in lookup cmp dic <*> toPresburgerExp subst a- <*> toPresburgerExp subst b-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---- simplTypeCmp :: Type -> Type--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-+plugin = pluginWith defaultTranslation
+ src/GHC/TypeLits/Presburger/Compat.hs view
@@ -0,0 +1,549 @@+{- HLINT ignore "Use camelCase" -}+{- HLINT ignore "Move filter" -}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where++import Data.Coerce (coerce)+import Data.Function (on)+import Data.Functor ((<&>))+import Data.Generics.Twins+import GHC.TypeLits.Presburger.Flags+import GHC.Types.Unique as GHC.TypeLits.Presburger.Compat (Unique, getUnique)+import qualified GHC.Types.Unique as Unique (Unique, getKey)+#if MIN_VERSION_ghc(9,10,1)+import GHC.Builtin.Names (gHC_INTERNAL_TYPENATS, gHC_INTERNAL_TYPEERROR)+import GHC.Builtin.Names (mkGhcInternalModule)+#else+import GHC.Builtin.Names (gHC_TYPENATS)+#if MIN_VERSION_ghc(9,4,1)+import GHC.Builtin.Names (gHC_TYPENATS, gHC_TYPEERROR)+#endif+#endif+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat+import GHC.Tc.Types.Origin as GHC.TypeLits.Presburger.Compat (CtOrigin (..))+import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (+ evByFiat,+ lookupModule,+ lookupName,+ tracePlugin,+ )+#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, Role(..))+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (Coercion)+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+#if MIN_VERSION_ghc(9,12,1)+-- mkBaseModule is not available in GHC 9.12.1++import GHC.Core.Reduction (reductionReducedType)+#elif MIN_VERSION_ghc(9,4,1)+import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (mkBaseModule)+import GHC.Core.Reduction (reductionReducedType)+#else+import qualified GHC.Builtin.Names as Old+#endif+import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (+ boolTyCon,+ eqTyConName,+ promotedEQDataCon,+ promotedGTDataCon,+ promotedLTDataCon,+ )+import qualified GHC.Builtin.Types as TysWiredIn+import GHC.Builtin.Types.Literals as GHC.TypeLits.Presburger.Compat+import GHC.Core.Class as GHC.TypeLits.Presburger.Compat (className, classTyCon)+import GHC.Core.FamInstEnv as GHC.TypeLits.Presburger.Compat+import GHC.Core.Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred (..), isEqPred, mkPrimEqPredRole)+import qualified GHC.Core.Predicate as Old (classifyPredType)+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))+import GHC.Core.TyCon as GHC.TypeLits.Presburger.Compat+import qualified GHC.Core.Type as Old+import GHC.Core.Unify as Old (tcUnifyTy)+import GHC.Data.FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS)+import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule (..), NoExtField (..))+import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs)+import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl (..), ImportDeclQualifiedStyle (..))+import GHC.Unit.Types (Module, UnitId, toUnitId)+import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (mkModule)+#if MIN_VERSION_ghc(9,2,0)+import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))+#if !MIN_VERSION_ghc(9,12,1)+import GHC.Builtin.Names (mkBaseModule)+#endif+#else+import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))+import GHC.Driver.Session (unitState, unitDatabases)+#endif+import GHC.Plugins (InScopeSet, Name, Outputable, Unit, emptyUFM, moduleUnit)+#if MIN_VERSION_ghc(9,2,0)+import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsParsedModule(..))+import GHC.Types.TyThing as GHC.TypeLits.Presburger.Compat (lookupTyCon)+import GHC.Builtin.Types (naturalTy)+#else+import GHC.Plugins as GHC.TypeLits.Presburger.Compat + ( HsParsedModule(..),+ lookupTyCon,+ typeNatKind+ )+#endif++#if MIN_VERSION_ghc(9,6,1)+import GHC.Plugins as GHC.TypeLits.Presburger.Compat+ ( Subst (..),+ emptySubst,+ unionSubst,+ )+import GHC.Core.TyCo.Compare as GHC.TypeLits.Presburger.Compat+ (eqType)+#else+import GHC.Plugins as GHC.TypeLits.Presburger.Compat+ ( TCvSubst (..),+ emptyTCvSubst,+ eqType,+ unionTCvSubst,+ )+#endif++import GHC.Core.InstEnv as GHC.TypeLits.Presburger.Compat (classInstances)+import GHC.Plugins as GHC.TypeLits.Presburger.Compat (+ GenericUnitInfo (..),+ Hsc,+ PackageName (..),+ Plugin (..),+ TvSubstEnv,+ TyVar,+ UnitDatabase (..),+ consDataCon,+ defaultPlugin,+ elementOfUniqSet,+ isNumLitTy,+ isStrLitTy,+ mkTcOcc,+ mkTyConTy,+ mkTyVarTy,+ mkUniqSet,+ nilDataCon,+ ppr,+ promotedFalseDataCon,+ promotedTrueDataCon,+ purePlugin,+ splitTyConApp,+ splitTyConApp_maybe,+ text,+ tyConAppTyCon_maybe,+ typeKind,+ )+import GHC.Tc.Plugin (lookupOrig)+#if MIN_VERSION_ghc(9,2,0)+import GHC.Tc.Plugin (unsafeTcPluginTcM)+import GHC.Utils.Logger (getLogger)+import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..))+#else+import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..))+#endif++import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat (+ TcPluginM,+ getInstEnvs,+ getTopEnv,+ lookupOrig,+ matchFam,+ newFlexiTyVar,+ newWanted,+ tcLookupClass,+ tcLookupTyCon,+ tcPluginIO,+ tcPluginTrace,+ )+import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..))+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat (+ Ct,+ CtEvidence,+ ctEvPred,+ ctEvidence,+ isWanted,+ )+import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (EvTerm)+import GHC.Tc.Utils.Monad as GHC.TypeLits.Presburger.Compat (getCtLocM, unsafeTcPluginTcM)+import GHC.Tc.Utils.TcType (TcTyVar, TcType)+import GHC.Tc.Utils.TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts)+import qualified GHC.TcPluginM.Extra as Extra+import GHC.Types.Name.Occurrence as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc)+import GHC.Unit.Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName)+import GHC.Unit.State (UnitState (preloadUnits), initUnits)+import GHC.Unit.State as GHC.TypeLits.Presburger.Compat (lookupPackageName)+import GHC.Unit.Types (UnitId (..), fsToUnit, toUnitId)+import GHC.Utils.Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe)++#if !MIN_VERSION_ghc(9,4,1)+type TcPluginSolveResult = TcPluginResult+#endif++-- mkUnivCo API compatibility+#if MIN_VERSION_ghc(9,12,1)+mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion +mkUnivCo' prov role ty1 ty2 = mkUnivCo prov [] role ty1 ty2+#else+mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion +mkUnivCo' = mkUnivCo+#endif++#if MIN_VERSION_ghc(9,10,1)+dATA_TYPE_EQUALITY :: Module+dATA_TYPE_EQUALITY = mkGhcInternalModule "GHC.Internal.Data.Type.Equality"+#else+dATA_TYPE_EQUALITY :: Module+dATA_TYPE_EQUALITY = mkBaseModule "Data.Type.Equality"+#endif++#if MIN_VERSION_ghc(9,10,1)+gHC_TYPEERROR :: Module+gHC_TYPEERROR = gHC_INTERNAL_TYPEERROR++gHC_TYPENATS :: Module+gHC_TYPENATS = gHC_INTERNAL_TYPENATS+#elif !MIN_VERSION_ghc(9,4,1)+gHC_TYPEERROR :: Module+gHC_TYPEERROR = mkBaseModule "GHC.TypeLits"+#endif++type PredTree = Pred++data TvSubst = TvSubst InScopeSet TvSubstEnv++#if MIN_VERSION_ghc(9,6,1)+type TCvSubst = Subst+unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst+unionTCvSubst = unionSubst++emptyTCvSubst :: Subst+emptyTCvSubst = emptySubst+#endif++instance Outputable TvSubst where+ ppr = ppr . toTCv++emptyTvSubst :: TvSubst+#if MIN_VERSION_ghc(9,6,1)+emptyTvSubst = case emptyTCvSubst of+ Subst set _ tvsenv _ -> TvSubst set tvsenv+#else+emptyTvSubst = case emptyTCvSubst of+ TCvSubst set tvsenv _ -> TvSubst set tvsenv+#endif++toTCv :: TvSubst -> TCvSubst+#if MIN_VERSION_ghc(9,6,1)+toTCv (TvSubst set tvenv) = Subst set emptyUFM tvenv emptyUFM+#else+toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM+#endif++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+#if MIN_VERSION_ghc(9,6,1)+fromTCv (Subst set _ tvsenv _) = TvSubst set tvsenv+#else+fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv+#endif++promotedBoolTyCon :: TyCon+promotedBoolTyCon = boolTyCon++viewFunTy :: Type -> Maybe (Type, Type)+viewFunTy t@(TyConApp _ [t1, t2])+ | Old.isFunTy t = Just (t1, t2)+viewFunTy _ = Nothing++tcUnifyTy :: Type -> Type -> Maybe TvSubst+tcUnifyTy t1 t2 = fromTCv <$> Old.tcUnifyTy t1 t2++getEqTyCon :: TcPluginM TyCon+getEqTyCon =+ return TysWiredIn.eqTyCon++getEqWitnessTyCon :: TcPluginM TyCon+getEqWitnessTyCon = do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc ":~:")++getEqBoolTyCon :: TcPluginM TyCon+getEqBoolTyCon = do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc "==")++decompFunTy :: Type -> [Type]+decompFunTy (FunTy _ _ t1 t2) = t1 : decompFunTy t2+decompFunTy t = [t]++newtype TypeEq = TypeEq {runTypeEq :: Type}++instance Eq TypeEq where+ (==) = geq `on` runTypeEq++instance Ord TypeEq where+ compare = gcompare `on` runTypeEq++isTrivial :: Old.PredType -> Bool+isTrivial ty =+ case classifyPredType ty of+ EqPred _ l r -> l `eqType` r+ _ -> False++normaliseGivens ::+ [Ct] -> TcPluginM [Ct]+normaliseGivens =+ fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence))+ . (++)+ <$> id+ <*> Extra.flattenGivens++#if MIN_VERSION_ghc(8,4,1)+type Substitution = [(TcTyVar, TcType)]+#else+type Substitution = TvSubst+#endif++subsCt :: Substitution -> Ct -> Ct+subsCt = Extra.substCt++subsType :: Substitution -> Type -> Type+subsType = Extra.substType++mkSubstitution :: [Ct] -> Substitution+mkSubstitution = map fst . Extra.mkSubst'++classifyPredType :: Type -> PredTree+classifyPredType ty = case Old.classifyPredType ty of+ e@EqPred {} -> e+ ClassPred cls [_, t1, t2]+ | className cls == eqTyConName ->+ EqPred NomEq t1 t2+ e -> e++fsToUnitId :: FastString -> UnitId+fsToUnitId = toUnitId . fsToUnit++loadedPackageNames ::+ [UnitDatabase UnitId] ->+ UnitState ->+ [RawPackageName]+loadedPackageNames unitDb us =+ let preloads = mkUniqSet $ map (\(UnitId p) -> p) $ preloadUnits us+ ents = filter ((`elementOfUniqSet` preloads) . unitIdFS . unitId) $ concatMap unitDatabaseUnits unitDb+ in map (coerce . unitPackageName) ents++type RawPackageName = FastString++preloadedUnitsM :: TcPluginM [RawPackageName]+#if MIN_VERSION_ghc(9,4,0)+preloadedUnitsM = do+ logger <- unsafeTcPluginTcM getLogger+ dflags <- hsc_dflags <$> getTopEnv+ packNames <- tcPluginIO $ initUnits logger dflags Nothing mempty <&> + \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us+ tcPluginTrace "pres: packs" $ ppr packNames+ pure $ coerce packNames+#elif MIN_VERSION_ghc(9,2,0)+preloadedUnitsM = do+ logger <- unsafeTcPluginTcM getLogger+ dflags <- hsc_dflags <$> getTopEnv+ packNames <- tcPluginIO $ initUnits logger dflags Nothing <&> + \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us+ tcPluginTrace "pres: packs" $ ppr packNames+ pure packNames+#elif MIN_VERSION_ghc(9,0,0)+preloadedUnitsM = do+ dflags <- hsc_dflags <$> getTopEnv+ packNames <- tcPluginIO $ initUnits dflags <&> \dfs' ->+ let st = unitState dfs'+ db = maybe [] id $ unitDatabases dfs'+ in loadedPackageNames db st+ tcPluginTrace "pres: packs" $ ppr packNames+ pure packNames+#else+preloadedUnitsM = do+ dflags <- hsc_dflags <$> getTopEnv+ (dfs', packs) <- tcPluginIO $ initPackages dflags+ let db = listPackageConfigMap dfs'+ loadeds = mkUniqSet $ map (\(InstalledUnitId p) -> p) packs+ packNames = map (coerce . packageName) $+ filter ((`elementOfUniqSet` loadeds) . coerce . unitId) db+ tcPluginTrace "pres: packs" $ ppr packNames+ pure packNames+#endif++type ModuleUnit = Unit++moduleUnit' :: Module -> ModuleUnit+moduleUnit' = moduleUnit++noExtField :: NoExtField+noExtField = NoExtField++type HsModule' = HsModule++#if MIN_VERSION_ghc(9,2,0)+typeNatKind :: TcType+typeNatKind = naturalTy+#endif++mtypeNatLeqTyCon :: Maybe TyCon+#if MIN_VERSION_ghc(9,2,0)+mtypeNatLeqTyCon = Nothing+#else+mtypeNatLeqTyCon = Just typeNatLeqTyCon+#endif++dATA_TYPE_ORD :: Module+#if MIN_VERSION_ghc(9,10,0)+dATA_TYPE_ORD = mkGhcInternalModule "GHC.Internal.Data.Type.Ord"+#else+dATA_TYPE_ORD = mkBaseModule "Data.Type.Ord"+#endif++lookupTyNatPredLeq :: TcPluginM Name+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatPredLeq = lookupOrig dATA_TYPE_ORD (mkTcOcc "<=")+#else+lookupTyNatPredLeq = + lookupOrig gHC_TYPENATS (mkTcOcc "<=")+#endif++lookupTyNatBoolLeq :: TcPluginM TyCon+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatBoolLeq = tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "<=?")+#else+lookupTyNatBoolLeq = + pure typeNatLeqTyCon+#endif++lookupAssertTyCon :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_base(4,17,0)+lookupAssertTyCon = + fmap Just . tcLookupTyCon =<< lookupOrig gHC_TYPEERROR (mkTcOcc "Assert")+#else+lookupAssertTyCon = pure Nothing+#endif++lookupTyNatPredLt :: TcPluginM (Maybe TyCon)++-- Note: base library shipepd with 9.2.1 has a wrong implementation;+-- hence we MUST NOT desugar it with <= 9.2.1+#if MIN_VERSION_ghc(9,2,2)+lookupTyNatPredLt = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "<")+#else+lookupTyNatPredLt = pure Nothing+#endif++lookupTyNatBoolLt :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatBoolLt = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "<?")+#else+lookupTyNatBoolLt = pure Nothing+#endif++lookupTyNatPredGt :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatPredGt = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">")+#else+lookupTyNatPredGt = pure Nothing+#endif++lookupTyNatBoolGt :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatBoolGt = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">?")+#else+lookupTyNatBoolGt = pure Nothing+#endif++lookupTyNatPredGeq :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatPredGeq = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">=")+#else+lookupTyNatPredGeq = pure Nothing+#endif++lookupTyNatBoolGeq :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatBoolGeq = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc ">=?")+#else+lookupTyNatBoolGeq = pure Nothing+#endif++mOrdCondTyCon :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+mOrdCondTyCon = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "OrdCond")+#else+mOrdCondTyCon = pure Nothing+#endif++lookupTyGenericCompare :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+lookupTyGenericCompare = Just <$> do+ tcLookupTyCon =<< lookupOrig dATA_TYPE_ORD (mkTcOcc "Compare")+#else+lookupTyGenericCompare = pure Nothing+#endif++lookupBool47 :: String -> TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,10,0)+lookupBool47 nam = Just <$> do+ tcLookupTyCon =<< lookupOrig (mkGhcInternalModule "GHC.Internal.Data.Type.Bool") (mkTcOcc nam)+#elif MIN_VERSION_base(4,17,0)+lookupBool47 nam = Just <$> do+ tcLookupTyCon =<< lookupOrig (mkBaseModule "Data.Type.Bool") (mkTcOcc nam)+#else+lookupBool47 = const $ pure Nothing+#endif++lookupTyNot, lookupTyIf, lookupTyAnd, lookupTyOr :: TcPluginM (Maybe TyCon)+lookupTyNot = lookupBool47 "Not"+lookupTyIf = lookupBool47 "If"+lookupTyAnd = lookupBool47 "&&"+lookupTyOr = lookupBool47 "||"++matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe Type)+#if MIN_VERSION_ghc(9,4,1)+matchFam' con args = fmap reductionReducedType <$> matchFam con args+#else+matchFam' con args = fmap snd <$> matchFam con args +#endif++getKey :: Unique.Unique -> Int+getKey = fromIntegral . Unique.getKey++getVoidTyCon :: TcPluginM TyCon+getVoidTyCon = tcLookupTyCon =<< lookupOrig aMod (mkTcOcc "Void")+ where+#if MIN_VERSION_ghc(9,10,1)+ aMod = mkGhcInternalModule "GHC.Internal.Base"+#elif MIN_VERSION_ghc(9,6,1)+ aMod = mkBaseModule "GHC.Base"+#else+ aMod = mkBaseModule "Data.Void"+#endif
+ src/GHC/TypeLits/Presburger/Flags.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE CPP #-}+module GHC.TypeLits.Presburger.Flags (GHCVer(..), ghcVer) where+import GHC.Generics (Generic)++data GHCVer + = GHC806 | GHC808 | GHC810 + | GHC900 | GHC902 | GHC904 + | GHC906 | GHC908 | GHC910+ deriving (Show, Eq, Ord, Generic)++ghcVer :: GHCVer+#if MIN_VERSION_ghc(9,10,1)+ghcVer = GHC910+#elif MIN_VERSION_ghc(9,8,1)+ghcVer = GHC908+#elif MIN_VERSION_ghc(9,6,1)+ghcVer = GHC906+#elif MIN_VERSION_ghc(9,4,1)+ghcVer = GHC904+#elif MIN_VERSION_ghc(9,2,1)+ghcVer = GHC902+#elif MIN_VERSION_ghc(9,0,1)+ghcVer = GHC900+#elif MIN_VERSION_ghc(8,10,1)+ghcVer = GHC810+#elif MIN_VERSION_ghc(8,8,1)+ghcVer = GHC808+#else+ghcVer = GHC806+#endif
+ src/GHC/TypeLits/Presburger/Types.hs view
@@ -0,0 +1,773 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE DerivingStrategies #-}+{-# 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,+ defaultTranslation,+ Translation (..),+ ParseEnv,+ Machine,+ module Data.Integer.SAT,+ )+where++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.Char (isDigit)+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)+#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+ ( catMaybes,+ fromMaybe,+ isNothing,+ listToMaybe,+ maybeToList,+ )+import Data.Reflection (Given, give, given)+import qualified Data.Set as Set+import GHC.TypeLits.Presburger.Compat as Compat+import qualified Data.Foldable as F+import GHC.TypeLits.Presburger.Flags++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 (Min l r) = nub $ varsExpr l ++ varsExpr r+varsExpr (Max l r) = nub $ varsExpr l ++ varsExpr r+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++data PluginMode+ = DisallowNegatives+ | AllowNegatives+ deriving (Read, Show, Eq, Ord)++pluginWith :: TcPluginM Translation -> Plugin+pluginWith trans =+ defaultPlugin+ { tcPlugin = Just . presburgerPlugin trans . procOpts+ , pluginRecompile = purePlugin+ }+ where+ procOpts opts+ | "allow-negated-numbers" `elem` opts = AllowNegatives+ | otherwise = DisallowNegatives++presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin+presburgerPlugin trans mode =+ tracePlugin+ "typelits-presburger"+ TcPlugin+ { tcPluginInit = return ()+ , tcPluginStop = const $ return ()+#if MIN_VERSION_ghc(9,4,1)+ , tcPluginSolve = const $ \_ gs ws -> decidePresburger mode trans () gs [] ws+#else+ , tcPluginSolve = decidePresburger mode trans+#endif++#if MIN_VERSION_ghc(9,4,1)+ , tcPluginRewrite = mempty+#endif+ }++testIf :: PropSet -> Prop -> Proof+testIf ps q = maybe Proved Disproved $ checkSat (Not q `assert'` ps)++-- Replaces every subtraction with new constant,+-- adding order constraint.+handleSubtraction :: PluginMode -> Prop -> Prop+handleSubtraction AllowNegatives p = p+handleSubtraction DisallowNegatives p0 =+ let (p, _, w) = runRWS (loop p0) () Set.empty+ in foldr (:&&) p w+ where+ 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 (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+ modify $ Set.insert pos+ tell $ Set.fromList [pos :>= K 0]+ return pos++ loopExp e@(Negate _) = withPositive . Negate =<< loopExp e+ loopExp (l :- r) = do+ e <- (:-) <$> loopExp l <*> loopExp r+ withPositive e+ 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 (Min l r) = Min <$> loopExp l <*> loopExp r+ loopExp (Max l r) = Max <$> loopExp l <*> loopExp r+ loopExp (If p l r) = If <$> loop p <*> loopExp l <*> loopExp r+ loopExp (Mod l n) = Mod <$> loopExp l <*> pure n+ loopExp (Div l n) = Div <$> loopExp l <*> pure n+ loopExp e@(K _) = return e++data Translation = Translation+ { isEmpty :: [TyCon]+ , ordCond :: [TyCon]+ , assertTy :: [TyCon]+ , isTrue :: [TyCon]+ , trueData :: [TyCon]+ , falseData :: [TyCon]+ , voids :: [TyCon]+ , tyEq :: [TyCon]+ , tyEqBool :: [TyCon]+ , tyEqWitness :: [TyCon]+ , tyNot :: [TyCon]+ , tyAnd :: [TyCon]+ , tyOr :: [TyCon]+ , tyIf :: [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]+ , natMin :: [TyCon]+ , natMax :: [TyCon]+ , orderingLT :: [TyCon]+ , orderingGT :: [TyCon]+ , orderingEQ :: [TyCon]+ , natCompare :: [TyCon]+ , parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop+ , parseExpr :: (Type -> Machine Expr) -> Type -> Machine Expr+ }++instance Semigroup Translation where+ l <> r =+ Translation+ { isEmpty = isEmpty l <> isEmpty r+ , isTrue = isTrue l <> isTrue r+ , assertTy = assertTy l <> assertTy r+ , voids = voids l <> voids r+ , tyEq = tyEq l <> tyEq r+ , tyNot = tyNot l <> tyNot r+ , tyAnd = tyAnd l <> tyAnd r+ , tyOr = tyOr l <> tyOr r+ , tyIf = tyIf l <> tyIf r+ , tyEqBool = tyEqBool l <> tyEqBool r+ , tyEqWitness = tyEqWitness l <> tyEqWitness r+ , tyNeqBool = tyNeqBool l <> tyNeqBool r+ , natPlus = natPlus l <> natPlus r+ , natMinus = natMinus l <> natMinus r+ , natTimes = natTimes l <> natTimes r+ , natExp = natExp l <> natExp r+ , natLeq = natLeq l <> natLeq r+ , natGeq = natGeq l <> natGeq r+ , natLt = natLt l <> natLt r+ , natGt = natGt l <> natGt r+ , natLeqBool = natLeqBool l <> natLeqBool r+ , natGeqBool = natGeqBool l <> natGeqBool r+ , natLtBool = natLtBool l <> natLtBool r+ , natGtBool = natGtBool l <> natGtBool r+ , orderingLT = orderingLT l <> orderingLT r+ , orderingGT = orderingGT l <> orderingGT r+ , orderingEQ = orderingEQ l <> orderingEQ r+ , natCompare = natCompare l <> natCompare r+ , trueData = trueData l <> trueData r+ , falseData = falseData l <> falseData r+ , parsePred = \f ty -> parsePred l f ty <|> parsePred r f ty+ , parseExpr = \toE -> (<|>) <$> parseExpr l toE <*> parseExpr r toE+ , natMin = natMin l <> natMin r+ , natMax = natMax l <> natMax r+ , ordCond = ordCond l <> ordCond r+ }++instance Monoid Translation where+ mempty =+ Translation+ { isEmpty = mempty+ , isTrue = mempty+ , assertTy = mempty+ , tyEq = mempty+ , tyEqBool = mempty+ , tyEqWitness = mempty+ , tyNeqBool = mempty+ , tyNot = mempty+ , tyAnd = mempty+ , tyOr = mempty+ , tyIf = 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 $ const mzero+ , natMin = mempty+ , natMax = mempty+ , ordCond = mempty+ }++decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult+decidePresburger _ genTrans _ gs [] [] = do+ tcPluginTrace "pres: Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs)+ trans <- genTrans+ give trans $ do+ ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred (deconsPred a)) gs+ let givens = catMaybes ngs+ prems0 = map snd givens+ prems = foldr assert' noProps prems0+ if isNothing (checkSat prems)+ then return $ TcPluginContradiction gs+ else return $ TcPluginOk [] []+decidePresburger mode genTrans _ gs _ds ws = do+ trans <- genTrans+ give trans $ do+ gs' <- normaliseGivens gs+ 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+ (prems, wants, prems0) <- do+ 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+ 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 =+ [ (evProof, ct)+ | ct <- solved+ , Just evProof <- pure $ extractProof $ 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+ Proved -> do+ tcPluginTrace "pres: Proved" (text $ show $ map snd wants)+ tcPluginTrace "pres: ... with coercions" (ppr coerced)+ return $ TcPluginOk coerced []+ Disproved wit -> do+ 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"++defaultTranslation :: TcPluginM Translation+defaultTranslation = do+ packs <- preloadedUnitsM+ let eqThere = elem eqReasoning packs+ (isEmpties, isTrues) <-+ if eqThere+ then do+ tcPluginTrace "pres: equational-reasoning activated!" $ ppr ()+ emd <- lookupModule (mkModuleName "Proof.Propositional.Empty") eqReasoning+ pmd <- lookupModule (mkModuleName "Proof.Propositional") eqReasoning++ emptyClsTyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))+ isTrueCon_ <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")+ pure ([emptyClsTyCon], [isTrueCon_])+ else do+ tcPluginTrace "pres: No equational-reasoning found." $ ppr ()+ pure ([], [])++ eqTyCon_ <- getEqTyCon+ eqBoolTyCon <- getEqBoolTyCon+ eqWitCon_ <- getEqWitnessTyCon+ assertTy <- lookupAssertTyCon+ voidTyCon <- getVoidTyCon+ nLeq <- tcLookupTyCon =<< lookupTyNatPredLeq+ tyLeqB <- lookupTyNatBoolLeq+ mTyLtP <- lookupTyNatPredLt+ mTyLtB <- lookupTyNatBoolLt+ mTyGeqP <- lookupTyNatPredGeq+ mTyGeqB <- lookupTyNatBoolGeq+ mTyGtP <- lookupTyNatPredGt+ mTyGtB <- lookupTyNatBoolGt+ mOrdCond <- mOrdCondTyCon+ mtyGenericCompare <- lookupTyGenericCompare+ tyNot <- maybeToList <$> lookupTyNot+ tyAnd <- maybeToList <$> lookupTyAnd+ tyOr <- maybeToList <$> lookupTyOr+ tyIf <- maybeToList <$> lookupTyIf+ let trans =+ mempty+ { isEmpty = isEmpties+ , assertTy = maybeToList assertTy+ , tyEq = [eqTyCon_]+ , tyNot+ , tyAnd+ , tyOr+ , tyIf+ , ordCond = F.toList mOrdCond+ , tyEqWitness = [eqWitCon_]+ , tyEqBool = [eqBoolTyCon]+ , isTrue = isTrues+ , voids = [voidTyCon]+ , natMinus = [typeNatSubTyCon]+ , natPlus = [typeNatAddTyCon]+ , natTimes = [typeNatMulTyCon]+ , natExp = [typeNatExpTyCon]+ , falseData = [promotedFalseDataCon]+ , trueData = [promotedTrueDataCon]+ , natLeqBool = [tyLeqB]+ , natLeq = [nLeq]+ , natGeqBool = F.toList mTyGeqB+ , natGeq = F.toList mTyGeqP+ , natGtBool = F.toList mTyGtB+ , natGt = F.toList mTyGtP+ , natLtBool = F.toList mTyLtB+ , natLt = F.toList mTyLtP+ , natCompare = typeNatCmpTyCon : F.toList mtyGenericCompare+ , orderingEQ = [promotedEQDataCon]+ , orderingLT = [promotedLTDataCon]+ , orderingGT = [promotedGTDataCon]+ }+ tcPluginTrace "Final translation: " (ppr mTyGeqB)+ pure trans++(<=>) :: Prop -> Prop -> Prop+p <=> q = (p :&& q) :|| (Not p :&& Not q)++orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)]+orderingDic =+ [(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 (lastN 2 -> [t1, t2]))+ | con `elem` (natLeq given ++ natLeqBool given) =+ (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPred (TyConApp con [t1, _])+ | con `elem` assertTy given = toPresburgerPred t1+toPresburgerPred ty+ | Just (con, []) <- splitTyConApp_maybe ty+ , con `elem` trueData given =+ return PTrue+ | Just (con, []) <- splitTyConApp_maybe ty+ , con `elem` falseData given =+ return PFalse+ | cls@(EqPred NomEq _ _) <- classifyPredType ty =+ toPresburgerPredTree cls+ | isEqPred ty = toPresburgerPredTree $ classifyPredType ty+ | Just (con, [l, r]) <- splitTyConAppLastBin ty -- 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+ | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ...+ , con `elem` isEmpty given =+ Not <$> toPresburgerPred l+ | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>+ , con `elem` isTrue given =+ toPresburgerPred l+ | Just (con, [l]) <- splitTyConApp_maybe ty -- Not p (from Data.Type.Bool)+ , con `elem` tyNot given =+ Not <$> toPresburgerPred l+ | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p && q (from Data.Type.Bool)+ , con `elem` tyAnd given =+ (:&&) <$> toPresburgerPred l <*> toPresburgerPred r+ | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p || q (from Data.Type.Bool)+ , con `elem` tyOr given =+ (:||) <$> toPresburgerPred l <*> toPresburgerPred r+ | Just (con, lastN 3 -> [p, t, f]) <- splitTyConApp_maybe ty -- If p t f (from Data.Type.Bool)+ , con `elem` tyIf given = do+ p' <- toPresburgerPred p+ (:||) + <$> ((p' :&&) <$> toPresburgerPred t) + <*> ((Not p':&&) <$> toPresburgerPred f)+ | Just (con, [t1, t2]) <- splitTyConAppLastBin ty+ , typeKind t1 `eqType` typeNatKind+ , typeKind t2 `eqType` typeNatKind + , Just p <- lookup con binPropDic =+ p <$> toPresburgerExp t1 <*> toPresburgerExp t2+ | Just DataCond{..} <- parseOrdCond ty = do -- OrdCond+ fromCondCases condCases+ <$> toPresburgerExp lhs+ <*> toPresburgerExp rhs+ | otherwise = parsePred given toPresburgerExp ty++splitTyConAppLastBin :: Type -> Maybe (TyCon, [Type])+splitTyConAppLastBin t = do+ (con, ts) <- splitTyConApp_maybe t+ let !n = length ts+ guard $ n >= 2+ return (con, drop (n - 2) ts)++data DataCond = DataCond { lhs, rhs :: Type, condCases :: CondCases }++data CondCases = CondCases { ltCase, eqCase, gtCase :: Bool }+ deriving (Show, Eq, Ord)++fromCondCases :: CondCases -> Expr -> Expr -> Prop+fromCondCases (CondCases True False False) = (:<)+fromCondCases (CondCases False True False) = (:==)+fromCondCases (CondCases False False True) = (:>)+fromCondCases (CondCases True True False) = (:<=)+fromCondCases (CondCases True False True) = (:/=)+fromCondCases (CondCases True True True) = const $ const PTrue+fromCondCases (CondCases False True True) = (:>=)+fromCondCases (CondCases False False False) = const $ const PFalse++parseOrdCond :: Given Translation => Type -> Maybe DataCond+parseOrdCond ty = do+ (con, lastN 4 -> [cmp, ltTy, eqTy, gtTy]) <- splitTyConApp_maybe ty+ guard $ con `elem` ordCond given+ (cmpCon, lastN 2 -> [lhs, rhs]) <- splitTyConApp_maybe cmp+ guard $ cmpCon `elem` natCompare given+ ltCase <- decodeTyBool ltTy+ eqCase <- decodeTyBool eqTy+ gtCase <- decodeTyBool gtTy+ let condCases = CondCases{..}+ pure DataCond{..}++decodeTyBool :: Type -> Maybe Bool+decodeTyBool ty = do+ con <- tyConAppTyCon_maybe ty+ (True <$ guard (con == promotedTrueDataCon))+ <|> (False <$ guard (con == promotedFalseDataCon))+++toPresburgerPredTree :: Given Translation => PredTree -> Machine Prop+toPresburgerPredTree (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True+ | maybe False (`elem` falseData given) $ tyConAppTyCon_maybe false =+ Not <$> toPresburgerPred p+toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'b+ | Just isTrue <- decodeTyBool b+ , Just (con, [t1, t2]) <- splitTyConAppLastBin p+ , con `elem` natLeqBool given =+ if isTrue + then (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+ else (:>) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPredTree (EqPred NomEq p b) -- (n :<? m) ~ b+ | Just isTrue <- decodeTyBool b+ , Just (con, [t1, t2]) <- splitTyConAppLastBin p+ , con `elem` natLtBool given =+ if isTrue + then (:<) <$> toPresburgerExp t1 <*> toPresburgerExp t2+ else (:>=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPredTree (EqPred NomEq p b) -- (n :>? m) ~ b+ | Just isTrue <- decodeTyBool b+ , Just (con, [t1, t2]) <- splitTyConAppLastBin p+ , con `elem` natGtBool given =+ if isTrue + then (:>) <$> toPresburgerExp t1 <*> toPresburgerExp t2+ else (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPredTree (EqPred NomEq p b) -- (n :>=? m) ~ b+ | Just isTrue <- decodeTyBool b+ , Just (con, [t1, t2]) <- splitTyConAppLastBin p+ , con `elem` natGeqBool given =+ if isTrue + then (:>=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+ else (:<) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPredTree (EqPred NomEq p b) + | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b =+ toPresburgerPred p+toPresburgerPredTree (EqPred NomEq b p) + | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b =+ toPresburgerPred p+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+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)+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 =+ MaybeT (return $ lookup cmp orderingDic)+ <*> 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 =+ MaybeT (return $ lookup cmp orderingDic)+ <*> toPresburgerExp a+ <*> toPresburgerExp b+toPresburgerPredTree (EqPred NomEq cond p) + -- OrdCond (CmpNat _ _) lt eq gt ~ ? (for GHC >= 9.2)+ | Just DataCond{..} <- parseOrdCond cond = do+ body <- fromCondCases condCases+ <$> toPresburgerExp lhs+ <*> toPresburgerExp rhs+ maybe ((body <=>) <$> toPresburgerPred p) + (\q -> if q then pure body else pure $ Not body)+ $ decodeTyBool p+ -- ? ~ OrdCond (CmpNat _ _) lt eq gt (for GHC >= 9.2)+ | Just DataCond{..} <- parseOrdCond p = do+ body <- fromCondCases condCases+ <$> toPresburgerExp lhs+ <*> toPresburgerExp rhs+ maybe ((body <=>) <$> toPresburgerPred cond) + (\q -> if q then pure body else pure $ Not body)+ $ decodeTyBool cond+toPresburgerPredTree (ClassPred con ts)+ -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)+ | [t1, t2] <- lastN 2 ts+ , typeKind t1 `eqType` typeNatKind+ , typeKind t2 `eqType` typeNatKind =+ let p = lookup (classTyCon con) binPropDic+ 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 <- tyEqBool given]++toPresburgerExp :: Given Translation => Type -> Machine Expr+toPresburgerExp ty = case ty of+ TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t+ TyConApp tc (lastN 3 -> [p, t, f])+ | tc `elem` tyIf given ->+ If <$> toPresburgerPred p <*> toPresburgerExp t <*> toPresburgerExp f + TyConApp tc (lastN 4 -> [cmpNM, l, e, g])+ | tc `elem` ordCond given+ , TyConApp cmp (lastN 2 -> [n, m]) <- cmpNM+ , cmp `elem` natCompare given+ , all ((`elem` [TypeEq n, TypeEq m]) . TypeEq) [l,e,g]+ -> decodeMinMax n m l e g+ t@(TyConApp tc ts) ->+ parseExpr given toPresburgerExp ty+ <|> body tc ts+ <|> Var . toName . getKey . getUnique <$> toVar t+ LitTy (NumTyLit n) -> return (K n)+ LitTy _ -> mzero+ t ->+ parseExpr given toPresburgerExp ty+ <|> Var . toName . getKey . getUnique <$> toVar t+ where+ body tc ts =+ let step con op+ | 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) -> (:*) n <$> toPresburgerExp x+ (x, LitTy (NumTyLit n)) -> (:*) n <$> toPresburgerExp x+ _ -> mzero+ _ ->+ asum $+ [ step con (:+)+ | con <- natPlus given+ ]+ ++ [ step con (:-)+ | con <- natMinus given+ ]+ ++ [ step con Min+ | con <- natMin given+ ]+ ++ [ step con Max+ | con <- natMin given+ ]++decodeMinMax :: Given Translation => Type -> Type -> Type -> Type -> Type -> Machine Expr+decodeMinMax n m lt eq gt + | lt `eqType` n && eq `eqType` n && gt `eqType` m = + Min <$> toPresburgerExp n <*> toPresburgerExp m+ | lt `eqType` n && eq `eqType` m && gt `eqType` m = + Min <$> toPresburgerExp n <*> toPresburgerExp m+ | lt `eqType` m && eq `eqType` m && gt `eqType` n = + Max <$> toPresburgerExp n <*> toPresburgerExp m+ | lt `eqType` m && eq `eqType` n && gt `eqType` n = + Max <$> toPresburgerExp n <*> toPresburgerExp m+ | otherwise = mzero++-- simplTypeCmp :: Type -> Type++lastTwo :: [a] -> [a]+lastTwo = drop <$> subtract 2 . length <*> id+lastN :: Int -> [a] -> [a]+lastN n = drop <$> subtract n . length <*> id++simpleExp :: Given Translation => Type -> Type+simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)+simpleExp (FunTy f m t1 t2) = FunTy f m (simpleExp t1) (simpleExp t2)+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]+ )+ 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++type ParseEnv = M.Map TypeEq TyVar++type Machine = MaybeT (StateT ParseEnv TcPluginM)+++runMachine :: Machine a -> TcPluginM (Maybe a)+runMachine act = do+ (ma, dic) <- runStateT (runMaybeT act) M.empty+ forM_ (M.toList dic) $ \(TypeEq ty, var) -> do+ loc <- unsafeTcPluginTcM $ getCtLocM (Shouldn'tHappenOrigin "runMachine dummy wanted") Nothing+ newWanted loc $ mkPrimEqPredRole Nominal (mkTyVarTy var) ty+ 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
+ test/ErrorsNoPlugin.hs view
@@ -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
+ test/ErrorsWithPlugin.hs view
@@ -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
+ test/GHC/TypeLits/PresburgerSpec.hs view
@@ -0,0 +1,70 @@+{-# 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)+ | any (`T.isInfixOf` T.pack msg)+ [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"+ , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"+ , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’"+ , "[GHC-25897]"+ ]+ -> 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)+ | any (`T.isInfixOf` T.pack msg)+ [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"+ , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"+ , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’"+ , "[GHC-25897]"+ ] -> 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)+ | any (`T.isInfixOf` T.pack msg )+ [ "Could not deduce: n1 ~ n"+ , "Could not deduce (n1 ~ n)"+ , "Could not deduce ‘n1 ~ n’"+ ]+ -> 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)+ | any (`T.isInfixOf` T.pack msg )+ [ "Could not deduce: n1 ~ n"+ , "Could not deduce (n1 ~ n)"+ , "Could not deduce ‘n1 ~ n’"+ ]+ -> pure ()+ _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith+ ]
@@ -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 :-
+ test/test.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover #-}