ghc-typelits-presburger 0.2.0.5 → 0.3.0.0

raw patch · 9 files changed

+1837/−1621 lines, 9 filesdep −singletonsdep ~equational-reasoningdep ~ghcdep ~ghc-tcplugins-extranew-component:exe:simple-arith-corePVP ok

version bump matches the API change (PVP)

Dependencies removed: singletons

Dependency ranges changed: equational-reasoning, ghc, ghc-tcplugins-extra

API changes (from Hackage documentation)

Files

• examples/simple-arith-core.hs +80/−0
• examples/simple-arith.hs +0/−77
• ghc-typelits-presburger.cabal +75/−56
• presburger/src/Data/Integer/SAT.hs +0/−981
• src/Data/Integer/SAT.hs +980/−0
• src/GHC/Compat.hs +0/−121
• src/GHC/TypeLits/Presburger.hs +7/−386
• src/GHC/TypeLits/Presburger/Compat.hs +194/−0
• src/GHC/TypeLits/Presburger/Types.hs +501/−0

@@ -0,0 +1,80 @@+{-# LANGUAGE CPP, DataKinds, EmptyCase, FlexibleContexts, GADTs, LambdaCase #-}+{-# LANGUAGE PolyKinds, ScopedTypeVariables, TypeFamilies, TypeInType       #-}+{-# LANGUAGE TypeOperators, UndecidableInstances                            #-}+{-# OPTIONS_GHC -dcore-lint #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806+{-# LANGUAGE NoStarIsType #-}+#endif++module Main where+import Data.Proxy+import Data.Type.Equality+import GHC.TypeLits+import Proof.Propositional (Empty (..), withEmpty)+import Proof.Propositional (IsTrue (Witness))++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 {}++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802+hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a+hoge _ Witness = absurdTrueFalse Refl+#endif++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++predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)+predSucc _ = Witness+++succLEqLTSucc :: pxy m -> CmpNat 0 (m + 1) :~: 'LT+succLEqLTSucc _ = Refl++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++main :: IO ()+main = putStrLn "finished"

@@ -1,77 +0,0 @@-{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-}-{-# LANGUAGE ScopedTypeVariables, CPP #-}-#if !MIN_VERSION_singletons(2,4,1)-{-# LANGUAGE KindSignatures #-}-#endif-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}-module Main where-import Data.Type.Equality-import GHC.TypeLits       (Nat, type (<=?), CmpNat)-import Proof.Propositional (Empty(..))-import Proof.Propositional (IsTrue(Witness))-import Data.Singletons.Prelude-import Data.Singletons.Prelude.List--#if !MIN_VERSION_singletons(2,4,1)-import qualified Data.Singletons.Prelude as Sing-type n <= m = (n :: Nat) Sing.:<= (m :: Nat)-infix 4 <=-type n - m = (n :: Nat) Sing.:- (m :: Nat)-infixl 6 --type n + m = (n :: Nat) Sing.:+ (m :: Nat)-infixl 6 +-type n * m = (n :: Nat) Sing.:* (m :: Nat)-infixl 7 *-#endif--type n <=! m = IsTrue (n <=? m)-infix 4 <=!--natLen :: (Length xs <= Length ys) ~ 'True-       => proxy xs -> proxy ys -> Length ys - Length xs + Length xs :~: Length ys-natLen _ _ = Refl--natLeqZero' :: ((n <= 0) ~ 'True) => proxy n -> n :~: 0-natLeqZero' _ = Refl--plusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m)-plusLeq _ _ = Refl--(%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)-n %:<=? m = case sCompare n m of-  SLT -> STrue-  SEQ -> STrue-  SGT -> SFalse--hoge :: ((n + 1 <=? n) ~ 'False) => proxy n -> ()-hoge _ = ()--hoge' :: (((n + 1) <= n) ~ 'False) => proxy n -> ()-hoge' _ = ()--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

@@ -1,61 +1,80 @@-name:                ghc-typelits-presburger-version:             0.2.0.5-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-                  -homepage:            https://github.com/konn/ghc-typelits-presburger#readme-license:             BSD3-license-file:        LICENSE-author:              Hiromi ISHII-maintainer:          konn.jinro _at_ gmail.com-copyright:           2015 (c) Hiromi ISHII-category:            Math, Type System-build-type:          Simple--- extra-source-files:-cabal-version:       >=1.10-tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3--flag examples-    Default: False+cabal-version: 1.12 -library-  ghc-options:         -Wall -Wno-dodgy-imports-  hs-source-dirs:      src-                     , presburger/src-  exposed-modules:     GHC.TypeLits.Presburger-  other-modules:       GHC.Compat-                       Data.Integer.SAT-  build-depends:       base                 >= 4.7  && < 5-                     , ghc                  >= 7.10 && < 8.5-                     , ghc-tcplugins-extra  >= 0.2  && < 0.4-                     , equational-reasoning >= 0.4.0.0-                     , singletons-                     , transformers-                     , mtl-                     , containers-                     , pretty-                     , syb-                     , reflection-  default-language:    Haskell2010+-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 213617ccefa67bad574a0687988e14cef38a75e07ac2e08140bcda55feeee3f6 -executable simple-arith-  if flag(examples)-    buildable:         True-  else-    buildable:         False-  hs-source-dirs:      examples-  Main-is:             simple-arith.hs-  build-depends:       base-                     , ghc-typelits-presburger-                     , equational-reasoning-                     , singletons-  default-language:    Haskell2010-  ghc-options:         -Wall -Wno-dodgy-imports -Wno-unused-imports+name:           ghc-typelits-presburger+version:        0.3.0.0+synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers.+description:    @ghc-typelits-presburger@ augments GHC type-system with Presburger+                Arithmetic Solver for Type-level natural numbers.+                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+maintainer:     konn.jinro _at_ gmail.com+copyright:      2015 (c) Hiromi ISHII+license:        BSD3+license-file:   LICENSE+tested-with:    GHC==8.4.3 GHC==8.6.3 GHC==8.8.2+build-type:     Simple  source-repository head-  type:     git+  type: git   location: https://github.com/konn/ghc-typelits-presburger++flag examples+  description: Builds example+  manual: False+  default: False++library+  exposed-modules:+      GHC.TypeLits.Presburger.Types+      GHC.TypeLits.Presburger+      GHC.TypeLits.Presburger.Compat+  other-modules:+      Data.Integer.SAT+      Paths_ghc_typelits_presburger+  hs-source-dirs:+      src+  ghc-options: -Wall -Wno-dodgy-imports+  build-depends:+      base >=4.7 && <5+    , containers+    , ghc >=7.10 && <8.11+    , ghc-tcplugins-extra >=0.2 && <0.4+    , mtl+    , pretty+    , reflection+    , syb+    , transformers+  default-language: Haskell2010++executable simple-arith-core+  main-is: simple-arith-core.hs+  other-modules:+      Paths_ghc_typelits_presburger+  hs-source-dirs:+      examples+  ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports+  build-depends:+      base+    , equational-reasoning+    , ghc-typelits-presburger+  if !(flag(examples))+    buildable: False+  default-language: Haskell2010

@@ -1,981 +0,0 @@-{-# LANGUAGE BangPatterns, PatternGuards, Trustworthy #-}-{-|-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 Debug.Trace--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           Prelude             hiding ((<>))-import           Text.PrettyPrint--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)---- | The type of integer expressions.--- Variable names must be non-negative.-data Expr = Expr :+ Expr          -- ^ Addition-          | Expr :- Expr          -- ^ Subtraction-          | Integer :* Expr       -- ^ Multiplication by a constant-          | Negate Expr           -- ^ Negation-          | Var Name              -- ^ Variable-          | K Integer             -- ^ Constant-          | If Prop Expr Expr     -- ^ A conditional expression-          | Div Expr Integer      -- ^ Division, rounds down-          | Mod Expr Integer      -- ^ Non-negative remainder-            deriving (Read,Show)--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 (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      = Bound Integer Term  -- ^ The integer is strictly positive-                  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-               -- -XC*x + S < 0-               -- S < XC*x-               then 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 ]-               -- XC*x + S < 0-               -- XC*x < -S-               else 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-  return a           = One a-  fail _             = None-  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  = return-  (<*>) = ap---newtype S a = S (RW -> Answer (a,RW))--instance Monad S where-  return a      = S $ \s -> return (a,s)-  S m >>= k     = S $ \s -> do (a,s1) <- m s-                               let S m1 = k a-                               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  = return-  (<*>) = 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.foldWithKey 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)-------

@@ -0,0 +1,980 @@+{-# LANGUAGE BangPatterns, CPP, PatternGuards, 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           Prelude             hiding ((<>))+import           Text.PrettyPrint++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 = Expr :+ Expr          -- ^ Addition+          | Expr :- Expr          -- ^ Subtraction+          | Integer :* Expr       -- ^ Multiplication by a constant+          | Negate Expr           -- ^ Negation+          | Var Name              -- ^ Variable+          | K Integer             -- ^ Constant+          | If Prop Expr Expr     -- ^ A conditional expression+          | Div Expr Integer      -- ^ Division, rounds down+          | Mod Expr Integer      -- ^ Non-negative remainder+            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 (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      = Bound Integer Term  -- ^ The integer is strictly positive+                  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+               -- -XC*x + S < 0+               -- S < XC*x+               then 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 ]+               -- XC*x + S < 0+               -- XC*x < -S+               else 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+  return a           = One a+#if !MIN_VERSION_ghc(8,8,1)+  fail _             = None+#endif+  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  = return+  (<*>) = ap+++newtype S a = S (RW -> Answer (a,RW))++instance Monad S where+  return a      = S $ \s -> return (a,s)+  S m >>= k     = S $ \s -> do (a,s1) <- m s+                               let S m1 = k a+                               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  = return+  (<*>) = 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)+++++++

@@ -1,121 +0,0 @@-{-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-}-{-# LANGUAGE TypeSynonymInstances, ViewPatterns                     #-}-{-# OPTIONS_GHC -Wno-orphans #-}-module GHC.Compat (module GHC.Compat) where-import Data.Function       (on)-import FamInst             as GHC.Compat-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 (typeNatKind)-import Module              as GHC.Compat (ModuleName, mkModuleName)-import OccName             as GHC.Compat (emptyOccSet, mkInstTyTcOcc)-import Plugins             as GHC.Compat (Plugin (..), defaultPlugin)-import TcEvidence          as GHC.Compat (EvTerm)-import TcHsType            as GHC.Compat (tcInferApps)-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 TcType              as GHC.Compat (tcTyFamInsts)-import TcTypeNats          as GHC.Compat-import TyCon               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           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 Data.Generics.Twins-import TcPluginM           (lookupOrig)-import TyCoRep             ()-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]--newtype TypeEq = TypeEq { runTypeEq :: Type }--instance Eq TypeEq where-  (==) = geq `on` runTypeEq--instance Ord TypeEq where-  compare = gcompare `on` runTypeEq

@@ -1,389 +1,10 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances      #-}-{-# LANGUAGE LambdaCase, MultiWayIf, OverloadedStrings, PatternGuards #-}-{-# LANGUAGE RankNTypes, RecordWildCards, TypeOperators               #-}-{-# LANGUAGE TypeSynonymInstances                                     #-}-{-# OPTIONS_GHC -Wno-unused-imports #-}+-- | Provides a plain Presburger solver plugin for @'GHC.TypeNats.Nat'@.+--+--   For an interface for extension, see+--   "GHC.TypeLits.Presburger.Types". module GHC.TypeLits.Presburger (plugin) where-import GHC.Compat--import           Class                     (Class, classTyCon)-import           Control.Applicative       ((<|>))-import           Control.Monad             (forM_, mzero)-import           Control.Monad.State.Class-import           Control.Monad.Trans.Class-import           Control.Monad.Trans.Maybe (MaybeT (..))-import           Control.Monad.Trans.State (StateT, runStateT)-import           Data.Foldable             (asum)-import           Data.Integer.SAT          (Expr (..), Prop (..), PropSet,-                                            assert)-import           Data.Integer.SAT          (checkSat, noProps, toName)-import qualified Data.Integer.SAT          as SAT-import           Data.List                 (nub)-import qualified Data.Map.Strict           as M-import qualified Data.Map.Strict           as M-import           Data.Maybe                (catMaybes, fromJust)-import           Data.Maybe                (fromMaybe, isNothing, mapMaybe)-import           Data.Reflection           (Given, give, given)-import           GHC.TypeLits              (Nat)-import           Outputable                (showSDocUnsafe)-import           TcPluginM                 (getFamInstEnvs, lookupOrig,-                                            matchFam, newFlexiTyVar, newWanted,-                                            tcLookupClass, unsafeTcPluginTcM)-import           TcRnTypes-import           TyCoRep                   (Coercion (..), KindCoercion (..))-import           Type                      (mkPrimEqPredRole, mkTyVarTy,-                                            splitTyConApp)-import           TysWiredIn                (promotedEQDataCon,-                                            promotedGTDataCon,-                                            promotedLTDataCon)-import           Var--assert' :: Prop -> PropSet -> PropSet-assert' p ps = foldr assert ps (p : varPos)-  where-    varPos = [K 0 :<= Var i | i <- varsProp p ]--data Proof = Proved | Disproved [(Int, Integer)]-           deriving (Read, Show, Eq, Ord)--isProved :: Proof -> Bool-isProved Proved = True-isProved _      = False--varsProp :: Prop -> [SAT.Name]-varsProp (p :|| q) = nub $ varsProp p ++ varsProp q-varsProp (p :&& q) = nub $ varsProp p ++ varsProp q-varsProp (Not p)   = varsProp p-varsProp (e :== v) = nub $ varsExpr e ++ varsExpr v-varsProp (e :/= v) = nub $ varsExpr e ++ varsExpr v-varsProp (e :< v)  = nub $ varsExpr e ++ varsExpr v-varsProp (e :> v)  = nub $ varsExpr e ++ varsExpr v-varsProp (e :<= v) = nub $ varsExpr e ++ varsExpr v-varsProp (e :>= v) = nub $ varsExpr e ++ varsExpr v-varsProp _         = []--varsExpr :: Expr -> [SAT.Name]-varsExpr (e :+ v)   = nub $ varsExpr e ++ varsExpr v-varsExpr (e :- v)   = nub $ varsExpr e ++ varsExpr v-varsExpr (_ :* v)   = varsExpr v-varsExpr (Negate e) = varsExpr e-varsExpr (Var i)    = [i]-varsExpr (K _)      = []-varsExpr (If p e v) = nub $ varsProp p ++ varsExpr e ++ varsExpr v-varsExpr (Div e _)  = varsExpr e-varsExpr (Mod e _)  = varsExpr e+import GHC.TypeLits.Presburger.Types+import GhcPlugins  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-                    , typeLeqBoolTyCon_   :: TyCon-                    , singCompareCon_     :: TyCon-                    , caseNameForSingLeq_ :: TyCon-                    , caseNameForSingGeq_ :: TyCon-                    , caseNameForSingLt_  :: TyCon-                    , caseNameForSingGt_  :: TyCon-                    }-caseNameForSingLeq :: Given MyEnv => TyCon-caseNameForSingLeq = caseNameForSingLeq_ given-caseNameForSingGeq :: Given MyEnv => TyCon-caseNameForSingGeq = caseNameForSingGeq_ given-caseNameForSingLt  :: Given MyEnv => TyCon-caseNameForSingLt = caseNameForSingLt_ given-caseNameForSingGt  :: Given MyEnv => TyCon-caseNameForSingGt = caseNameForSingGt_ given--eqTyCon :: Given MyEnv => TyCon-eqTyCon = eqTyCon_ given--eqWitnessTyCon :: Given MyEnv => TyCon-eqWitnessTyCon = eqWitCon_ given--isTrueTyCon :: Given MyEnv => TyCon-isTrueTyCon = isTrueCon_ given--typeLeqBoolTyCon :: Given MyEnv => TyCon-typeLeqBoolTyCon = typeLeqBoolTyCon_ given--singCompareCon :: Given MyEnv => TyCon-singCompareCon = singCompareCon_ 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-    ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred subst (deconsPred a)) gs-    let givens = catMaybes ngs-        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 . genSubst) emptyTvSubst (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-  (prems, wants) <- do-    wants <- catMaybes <$>-             mapM-             (\ct -> runMachine $ (,) ct <$> toPresburgerPred subst (substTy subst $ deconsPred ct))-             (filter (isWanted . ctEvidence) ws)-    resls <- mapM (runMachine . toPresburgerPred subst . substTy subst . deconsPred)-                     (gs ++ ds)-    let prems = foldr assert' noProps $ catMaybes resls-    return (prems, wants)-  let solved = map fst $ filter (isProved . testIf prems . snd) wants-      coerced = [(evByFiat "ghc-typelits-presburger" t1 t2, ct)-                | ct <- solved-                , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)-                ]-  -- tcPluginTrace "prems" (text $ show $ map (toPresburgerPred subst .substTy subst . deconsPred) (gs ++ ds))-  tcPluginTrace "final goals" (text $ show $ map snd wants)-  case testIf prems (foldr ((:&&) . snd) PTrue 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")-  emptyClsTyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))-  eqTyCon_ <- getEqTyCon-  eqWitCon_ <- getEqWitnessTyCon-  pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")-  isTrueCon_ <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")-  vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")-  voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")-  singletons <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")-#if MIN_VERSION_singletons(2,4,1)-  typeLeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "<=")-  typeLtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "<")-  typeGeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ">=")-  typeGtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ">")-#else-  typeLeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":<=")-  typeLtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":<")-  typeGeqBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":>=")-  typeGtBoolTyCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc ":>")-#endif-  caseNameForSingLeq_ <- getCaseNameForSingletonOp typeLeqBoolTyCon_-  caseNameForSingLt_ <- getCaseNameForSingletonOp typeLtBoolTyCon_-  caseNameForSingGeq_ <- getCaseNameForSingletonOp typeGeqBoolTyCon_-  caseNameForSingGt_ <- getCaseNameForSingletonOp typeGtBoolTyCon_-  singCompareCon_ <- tcLookupTyCon =<< lookupOrig singletons (mkTcOcc "Compare")-  give MyEnv{..} act--getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon-getCaseNameForSingletonOp con = do-  let vars = [typeNatKind, LitTy (NumTyLit 0), LitTy (NumTyLit 0)]-  Just (appTy0, [n,b,bdy,r]) <- fmap (splitTyConApp . snd) <$> matchFam  con vars-  let (appTy, args) = splitTyConApp bdy-  Just innermost <- fmap snd <$> matchFam appTy args-  Just (_, dat) <- matchFam appTy0 [n,b,innermost,r]-  Just dat' <- fmap snd <$> uncurry matchFam (splitTyConApp dat)-  return $ fst $ splitTyConApp dat'--(<=>) :: 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 -> Machine 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 = mzero--boolLeqs :: Given MyEnv => [TyCon]-boolLeqs = [typeNatLeqTyCon, typeLeqBoolTyCon]--toPresburgerPredTree :: Given MyEnv => TvSubst -> PredTree -> Machine 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 `elem` boolLeqs = (:<=) <$> toPresburgerExp subst t1  <*> toPresburgerExp subst t2-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's <=...-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p-  , con == caseNameForSingLeq-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =-    (:<=) <$> toPresburgerExp subst l <*> toPresburgerExp subst r-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's <...-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p-  , con == caseNameForSingLt-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =-    (:<) <$> toPresburgerExp subst l <*> toPresburgerExp subst r-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's >=...-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p-  , con == caseNameForSingGeq-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =-    (:>=) <$> toPresburgerExp subst l <*> toPresburgerExp subst r-  | Just promotedTrueDataCon  == tyConAppTyCon_maybe (substTy subst b) -- Singleton's >=...-  , Just (con, [_,_,_,_,cmpTy]) <- splitTyConApp_maybe p-  , con == caseNameForSingGt-  , Just (cmp, [l, r]) <- splitTyConApp_maybe cmpTy-  , cmp `elem` [singCompareCon, typeNatCmpTyCon] =-    (:>) <$> toPresburgerExp subst l <*> toPresburgerExp subst r-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 `elem` [singCompareCon, typeNatCmpTyCon], con' `elem` [typeNatCmpTyCon, singCompareCon]-  = (<=>) <$> ((:<) <$> 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 `elem` [typeNatCmpTyCon, singCompareCon]-  , Just cmp <- tyConAppTyCon_maybe (substTy subst t2) =-    let dic = [(promotedLTDataCon, (:<))-              ,(promotedEQDataCon, (:==))-              ,(promotedGTDataCon, (:>))-              ]-    in MaybeT (return $ 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 `elem` [singCompareCon, typeNatCmpTyCon]-  , Just cmp <- tyConAppTyCon_maybe (substTy subst t1) =-    let dic = [(promotedLTDataCon, (:<))-              ,(promotedEQDataCon, (:==))-              ,(promotedGTDataCon, (:>))-              ]-    in MaybeT (return $ 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 _ _ = mzero--toPresburgerExp :: TvSubst -> Type -> Machine Expr-toPresburgerExp dic ty = case substTy dic ty of-  TyVarTy t          -> return $ Var $ toName $ getKey $ getUnique t-  t@(TyConApp tc ts) -> body tc ts <|> Var . toName . getKey . getUnique <$> toVar t-  LitTy (NumTyLit n) -> return (K n)-  LitTy _            -> mzero-  t                  -> Var . toName . getKey .getUnique <$> toVar t-  where-    body tc ts =-      let step con op-            | tc == con, [tl, tr] <- ts =-              op <$> toPresburgerExp dic tl <*> toPresburgerExp dic tr-            | otherwise = mzero-      in case ts of-        [tl, tr] | tc == typeNatMulTyCon ->-          case (simpleExp tl, simpleExp tr) of-            (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m-            (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp dic x-            (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp dic x-            _ -> mzero-        _ ->  asum [ step con op-                   | (con, op) <- [(typeNatAddTyCon, (:+)), (typeNatSubTyCon, (:-))]]---- 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--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) ->-    newWanted undefined $ 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+plugin = pluginWith defaultTranslation

@@ -0,0 +1,194 @@+{-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-}+{-# LANGUAGE TypeSynonymInstances, ViewPatterns                     #-}+{-# OPTIONS_GHC -Wno-orphans #-}+module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where+import Data.Function       (on)+import FamInst             as GHC.TypeLits.Presburger.Compat+import FastString          as GHC.TypeLits.Presburger.Compat (fsLit)+import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName,+                                          tracePlugin)+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..))+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (classifyPredType, isEqPred,+                                          lookupTyCon, mkTyConTy)+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (mkTcOcc, ppr, promotedFalseDataCon)+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (promotedTrueDataCon, text)+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (tyConAppTyCon_maybe, typeKind)+import GhcPlugins          as GHC.TypeLits.Presburger.Compat (typeNatKind)+import Module              as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName)+import OccName             as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc)+import Plugins             as GHC.TypeLits.Presburger.Compat (Plugin (..), defaultPlugin)+import TcEvidence          as GHC.TypeLits.Presburger.Compat (EvTerm)+import TcHsType            as GHC.TypeLits.Presburger.Compat (tcInferApps)+import TcPluginM           as GHC.TypeLits.Presburger.Compat (TcPluginM, tcLookupTyCon,+                                          tcPluginTrace)+import TcRnMonad           as GHC.TypeLits.Presburger.Compat (Ct, TcPluginResult (..), isWanted)+import TcRnTypes           as GHC.TypeLits.Presburger.Compat (TcPlugin (..), ctEvPred, ctEvidence)+import TcType              as GHC.TypeLits.Presburger.Compat (tcTyFamInsts)+import TcTypeNats          as GHC.TypeLits.Presburger.Compat+import TyCon               as GHC.TypeLits.Presburger.Compat+#if MIN_VERSION_ghc(8,4,1)+import TcType (TcTyVar, TcType)+#else+import TcRnTypes (cc_ev, ctev_pred)+import Data.Maybe+import TcPluginM (zonkCt)+#endif+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800+import           GhcPlugins (InScopeSet, Outputable, emptyUFM)+import qualified PrelNames  as Old+import           TyCoRep    as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))+import           Type       as GHC.TypeLits.Presburger.Compat (TCvSubst (..), TvSubstEnv,+                                           emptyTCvSubst)+import           Type       as GHC.TypeLits.Presburger.Compat (eqType, unionTCvSubst)+import qualified Type       as Old+import           TysWiredIn as GHC.TypeLits.Presburger.Compat (boolTyCon)+import           Unify      as Old (tcUnifyTy)+#else+import Type       as GHC.TypeLits.Presburger.Compat (TvSubst, emptyTvSubst)+import Type       as GHC.TypeLits.Presburger.Compat (substTy, unionTvSubst)+import TypeRep    as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..))+import TysWiredIn as Old (eqTyCon)+import TysWiredIn as GHC.TypeLits.Presburger.Compat (promotedBoolTyCon)+import Unify      as GHC.TypeLits.Presburger.Compat (tcUnifyTy)+#endif+import Data.Generics.Twins+import TcPluginM           (lookupOrig)+import TyCoRep             ()+import Type                as GHC.TypeLits.Presburger.Compat (splitTyConApp_maybe)+import Unique              as GHC.TypeLits.Presburger.Compat (getKey, getUnique)+#if MIN_VERSION_ghc(8,4,1)+import qualified GHC.TcPluginM.Extra as Extra+#endif+#if MIN_VERSION_ghc(8,8,1)+import qualified TysWiredIn+#endif++#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 =+#if MIN_VERSION_ghc(8,8,1)+  return TysWiredIn.eqTyCon+#else+  tcLookupTyCon Old.eqTyConName+#endif++#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]++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 =+#if MIN_VERSION_ghc(8,4,1)+  fmap (return . filter (not . isTrivial . ctEvPred . ctEvidence)) +  . (++) <$> id <*> Extra.flattenGivens+#else+  mapM zonkCt +#endif++#if MIN_VERSION_ghc(8,4,1)+type Substitution = [(TcTyVar, TcType)]+#else+type Substitution = TvSubst+#endif++subsCt :: Substitution -> Ct -> Ct+subsCt =+#if MIN_VERSION_ghc(8,4,1)+  Extra.substCt+#else+  \subst ct ->+  ct { cc_ev = (cc_ev ct) {ctev_pred = substTy subst (ctev_pred (cc_ev ct))}+     }+#endif++subsType :: Substitution -> Type -> Type+subsType =+#if MIN_VERSION_ghc(8,4,1)+  Extra.substType+#else+  substTy+#endif++mkSubstitution :: [Ct] -> Substitution+mkSubstitution =+#if MIN_VERSION_ghc(8,4,1)+  fst . unzip . Extra.mkSubst'+#else+  foldr (unionTvSubst . genSubst) emptyTvSubst+#endif++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804+genSubst :: Ct -> TvSubst+genSubst ct = case classifyPredType (ctEvPred . ctEvidence $ ct) of+  EqPred NomEq t u -> fromMaybe emptyTvSubst $ GHC.TypeLits.Presburger.Compat.tcUnifyTy t u+  _                -> emptyTvSubst+#endif

@@ -0,0 +1,501 @@+{-# LANGUAGE BangPatterns, CPP, DataKinds, FlexibleContexts               #-}+{-# LANGUAGE FlexibleInstances, LambdaCase, MultiWayIf, OverloadedStrings #-}+{-# LANGUAGE PatternGuards, RankNTypes, TypeOperators, ViewPatterns       #-}+-- | Since 0.3.0.0+module GHC.TypeLits.Presburger.Types+  ( pluginWith+  , defaultTranslation+  , Translation(..), ParseEnv, Machine+  , module Data.Integer.SAT+  ) where+import           Class                          (classTyCon)+import           Control.Applicative            ((<|>))+import           Control.Arrow                  (second)+import           Control.Monad                  (forM_, guard, mzero, unless)+import           Control.Monad.State.Class+import           Control.Monad.Trans.Class+import           Control.Monad.Trans.Maybe      (MaybeT (..))+import           Control.Monad.Trans.RWS.Strict (runRWS, tell)+import           Control.Monad.Trans.State      (StateT, runStateT)+import           Data.Foldable                  (asum)+import           Data.Integer.SAT               (Expr (..), Prop (..), PropSet,+                                                 assert)+import           Data.Integer.SAT               (checkSat, noProps, toName)+import qualified Data.Integer.SAT               as SAT+import           Data.List                      (nub)+import qualified Data.Map.Strict                as M+import           Data.Maybe                     (catMaybes, fromMaybe,+                                                 isNothing)+import           Data.Reflection                (Given, give, given)+import qualified Data.Set                       as Set+import           GHC.TypeLits.Presburger.Compat+import           PrelNames+import           TcPluginM                      (lookupOrig, newFlexiTyVar,+                                                 newWanted, tcLookupClass)+import           Type                           (mkPrimEqPredRole, mkTyVarTy)+import           TysWiredIn                     (promotedEQDataCon,+                                                 promotedGTDataCon,+                                                 promotedLTDataCon)+import           Var+#if MIN_VERSION_ghc(8,6,0)+import Plugins (purePlugin)+#endif++assert' :: Prop -> PropSet -> PropSet+assert' p ps = foldr assert ps (p : varPos)+  where+    varPos = [K 0 :<= Var i | i <- varsProp p ]++data Proof = Proved | Disproved [(Int, Integer)]+           deriving (Read, Show, Eq, Ord)++isProved :: Proof -> Bool+isProved Proved = True+isProved _      = False++varsProp :: Prop -> [SAT.Name]+varsProp (p :|| q) = nub $ varsProp p ++ varsProp q+varsProp (p :&& q) = nub $ varsProp p ++ varsProp q+varsProp (Not p)   = varsProp p+varsProp (e :== v) = nub $ varsExpr e ++ varsExpr v+varsProp (e :/= v) = nub $ varsExpr e ++ varsExpr v+varsProp (e :< v)  = nub $ varsExpr e ++ varsExpr v+varsProp (e :> v)  = nub $ varsExpr e ++ varsExpr v+varsProp (e :<= v) = nub $ varsExpr e ++ varsExpr v+varsProp (e :>= v) = nub $ varsExpr e ++ varsExpr v+varsProp _         = []++varsExpr :: Expr -> [SAT.Name]+varsExpr (e :+ v)   = nub $ varsExpr e ++ varsExpr v+varsExpr (e :- v)   = nub $ varsExpr e ++ varsExpr v+varsExpr (_ :* v)   = varsExpr v+varsExpr (Negate e) = varsExpr e+varsExpr (Var i)    = [i]+varsExpr (K _)      = []+varsExpr (If p e v) = nub $ varsProp p ++ varsExpr e ++ varsExpr v+varsExpr (Div e _)  = varsExpr e+varsExpr (Mod e _)  = varsExpr e++data PluginMode = DisallowNegatives+                | AllowNegatives+                deriving (Read, Show, Eq, Ord)++pluginWith :: TcPluginM Translation -> Plugin+pluginWith trans = defaultPlugin+    { tcPlugin = Just . presburgerPlugin trans . procOpts+#if MIN_VERSION_ghc(8,6,0)+    , pluginRecompile = purePlugin+#endif+    }+  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 ()+           , tcPluginSolve = decidePresburger mode trans+           , tcPluginStop  = const $ return ()+           }++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 e@(K _) = return e++data Translation =+  Translation+    { isEmpty     :: [TyCon]+    , isTrue      :: [TyCon]+    , trueData    :: [TyCon]+    , falseData   :: [TyCon]+    , voids       :: [TyCon]+    , tyEq        :: [TyCon]+    , tyEqBool    :: [TyCon]+    , tyEqWitness :: [TyCon]+    , tyNeqBool   :: [TyCon]+    , natPlus     :: [TyCon]+    , natMinus    :: [TyCon]+    , natExp      :: [TyCon]+    , natTimes    :: [TyCon]+    , natLeq      :: [TyCon]+    , natLeqBool  :: [TyCon]+    , natGeq      :: [TyCon]+    , natGeqBool  :: [TyCon]+    , natLt       :: [TyCon]+    , natLtBool   :: [TyCon]+    , natGt       :: [TyCon]+    , natGtBool   :: [TyCon]+    , orderingLT  :: [TyCon]+    , orderingGT  :: [TyCon]+    , orderingEQ  :: [TyCon]+    , natCompare  :: [TyCon]+    , parsePred   :: (Type -> Machine Expr) -> Type -> Machine Prop+    , parseExpr   :: Type -> Machine Expr+    }++instance Semigroup Translation where+  l <> r =+    Translation+      { isEmpty = isEmpty l <> isEmpty r+      , isTrue = isTrue l <> isTrue r+      , voids = voids l <> voids r+      , tyEq = tyEq l <> tyEq 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 = (<|>) <$> parseExpr l <*> parseExpr r+      }++instance Monoid Translation where+  mempty = Translation+    { isEmpty = mempty+    , isTrue = mempty+    , tyEq  = mempty+    , tyEqBool = mempty+    , tyEqWitness = mempty+    , tyNeqBool = mempty+    , voids = mempty+    , natPlus = mempty+    , natMinus = mempty+    , natTimes = mempty+    , natExp = mempty+    , natLeq = mempty+    , natGeq = mempty+    , natLt = mempty+    , natGt = mempty+    , natLeqBool = mempty+    , natGeqBool = mempty+    , natLtBool = mempty+    , natGtBool = mempty+    , orderingLT = mempty+    , orderingGT = mempty+    , orderingEQ = mempty+    , natCompare = mempty+    , trueData = []+    , falseData = []+    , parsePred = const $ const mzero+    , parseExpr = const mzero+    }++decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult+decidePresburger _ genTrans _ gs [] [] = do+  tcPluginTrace "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+        (solved, _) = foldr go ([], noProps) givens+    if isNothing (checkSat prems)+      then return $ TcPluginContradiction gs+      else return $ TcPluginOk (map withEv solved) []+    where+      go (ct, p) (ss, prem)+        | Proved <- testIf prem p = (ct : ss, prem)+        | otherwise = (ss, assert' p prem)+decidePresburger mode genTrans _ gs ds ws = do+  trans <- genTrans+  give trans $ do+    gs' <- normaliseGivens gs+    let subst = mkSubstitution (gs' ++ ds)+    tcPluginTrace "Current subst" (ppr subst)+    tcPluginTrace "wanteds" $ ppr $ map deconsPred ws+    tcPluginTrace "givens" $ ppr $ map (subsType subst . deconsPred) gs+    tcPluginTrace "deriveds" $ ppr $ map deconsPred ds+    (prems, wants, prems0) <- do+      wants <- catMaybes <$>+              mapM+              (\ct -> runMachine $ (,) ct <$> toPresburgerPred+                  ( subsType subst+                  $ deconsPred $ subsCt subst ct))+              (filter (isWanted . ctEvidence) ws)++      resls <- mapM (runMachine . toPresburgerPred . subsType subst . deconsPred)+                      (gs ++ ds)+      let prems = foldr assert' noProps $ catMaybes resls+      return (prems, map (second $ handleSubtraction mode) wants, catMaybes resls)+    let solved = map fst $ filter (isProved . testIf prems . snd) wants+        coerced = [(evByFiat "ghc-typelits-presburger" t1 t2, ct)+                  | ct <- solved+                  , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)+                  ]+    tcPluginTrace "final premises" (text $ show prems0)+    tcPluginTrace "final goals" (text $ show $ map snd wants)+    case testIf prems (foldr ((:&&) . snd) PTrue wants) of+      Proved -> do+        tcPluginTrace "Proved" (text $ show $ map snd wants)+        tcPluginTrace "... with coercions" (ppr coerced)+        return $ TcPluginOk coerced []+      Disproved wit -> do+        tcPluginTrace "Failed! " (text $ show wit)+        return $ TcPluginContradiction $ map fst wants++defaultTranslation :: TcPluginM Translation+defaultTranslation = do+  emd <- lookupModule (mkModuleName "Proof.Propositional.Empty") (fsLit "equational-reasoning")+  emptyClsTyCon <- classTyCon <$> (tcLookupClass =<< lookupOrig emd (mkTcOcc "Empty"))+  eqTyCon_ <- getEqTyCon+  eqWitCon_ <- getEqWitnessTyCon+  pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")+  isTrueCon_ <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")+  vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")+  voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")+  nLeq <- tcLookupTyCon =<< lookupOrig gHC_TYPENATS (mkTcOcc "<=")+  return+    mempty+    { isEmpty = [emptyClsTyCon]+    , tyEq = [eqTyCon_]+    , tyEqWitness = [eqWitCon_]+    , isTrue = [isTrueCon_]+    , voids = [voidTyCon]+    , natMinus = [typeNatSubTyCon]+    , natPlus = [typeNatAddTyCon]+    , natTimes = [typeNatMulTyCon]+    , natExp = [typeNatExpTyCon]+    , falseData = [promotedFalseDataCon]+    , trueData = [promotedTrueDataCon]+    , natLeqBool = [typeNatLeqTyCon]+    , natLeq = [nLeq]+    , natCompare = [typeNatCmpTyCon]+    , orderingEQ = [promotedEQDataCon]+    , orderingLT = [promotedLTDataCon]+    , orderingGT = [promotedGTDataCon]+    }++(<=>) :: Prop -> Prop -> Prop+p <=> q =  (p :&& q) :|| (Not p :&& Not q)++withEv :: Ct -> (EvTerm, Ct)+withEv ct+  | EqPred _ t1 t2 <- classifyPredType (deconsPred ct) =+      (evByFiat "ghc-typelits-presburger" t1 t2, ct)+  | otherwise = undefined++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 [t1, t2])+  | con `elem` (natLeq given ++ natLeqBool given)+  = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPred ty+  | Just (con, []) <- splitTyConApp_maybe ty+  , con `elem` trueData given = return PTrue+  | Just (con, []) <- splitTyConApp_maybe ty+  , con `elem` falseData given = return PFalse+  | isEqPred ty = toPresburgerPredTree $ classifyPredType ty+  | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r+  , con `elem` (tyEq given ++ tyEqBool given)+  = toPresburgerPredTree $ EqPred NomEq l r+  | 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+  | 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)++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 <$> toPresburgerPredTree (EqPred NomEq p (mkTyConTy promotedTrueDataCon))+toPresburgerPredTree (EqPred NomEq p b)  -- (n :<=? m) ~ 'True+  | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b+  , Just (con, [t1, t2]) <- splitTyConAppLastBin p+  , con `elem` natLeqBool given = (:<=) <$> toPresburgerExp t1  <*> toPresburgerExp t2+toPresburgerPredTree (EqPred NomEq p q)  -- (p :: Bool) ~ (q :: Bool)+    | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do+      lift $ lift $ tcPluginTrace "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 (ClassPred con ts)+  -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)+  | let n = length ts, n >= 2+  , [t1, t2] <- drop (n - 2) ts+  , typeKind t1 `eqType` typeNatKind+  , typeKind t2 `eqType` typeNatKind =+    let 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 ]++toPresburgerExp :: Given Translation => Type -> Machine Expr+toPresburgerExp ty = case ty of+  TyVarTy t          -> return $ Var $ toName $ getKey $ getUnique t+  t@(TyConApp tc ts) -> body tc ts <|> Var . toName . getKey . getUnique <$> toVar t+  LitTy (NumTyLit n) -> return (K n)+  LitTy _            -> mzero+  t                  ->+        parseExpr given ty+    <|> Var . toName . getKey .getUnique <$> toVar t+  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) -> (:*) <$> pure n <*> toPresburgerExp x+            (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp x+            _ -> mzero+        _ ->  asum+           $  [ step con (:+)+              | con <- natPlus given+              ] +++              [ step con (:-)+              | con <- natMinus given+              ]+++-- simplTypeCmp :: Type -> Type++lastTwo :: [a] -> [a]+lastTwo = drop <$> subtract 2 . length <*> id++simpleExp :: Given Translation => 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 (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) ->+    newWanted undefined $ 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