{-# 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 Int -> PropSet -> ShowS
[PropSet] -> ShowS
PropSet -> String
(Int -> PropSet -> ShowS)
-> (PropSet -> String) -> ([PropSet] -> ShowS) -> Show PropSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropSet] -> ShowS
$cshowList :: [PropSet] -> ShowS
show :: PropSet -> String
$cshow :: PropSet -> String
showsPrec :: Int -> PropSet -> ShowS
$cshowsPrec :: Int -> PropSet -> ShowS
Show

dotPropSet :: PropSet -> Doc
dotPropSet :: PropSet -> Doc
dotPropSet (State Answer RW
a) = (RW -> Doc) -> Answer RW -> Doc
forall a. (a -> Doc) -> Answer a -> Doc
dotAnswer (Inerts -> Doc
ppInerts (Inerts -> Doc) -> (RW -> Inerts) -> RW -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> Inerts
inerts) Answer RW
a

sizePropSet :: PropSet -> (Integer,Integer,Integer)
sizePropSet :: PropSet -> (Integer, Integer, Integer)
sizePropSet (State Answer RW
a) = Answer RW -> (Integer, Integer, Integer)
forall a. Answer a -> (Integer, Integer, Integer)
answerSize Answer RW
a

-- | An empty collection of propositions.
noProps :: PropSet
noProps :: PropSet
noProps = Answer RW -> PropSet
State (Answer RW -> PropSet) -> Answer RW -> PropSet
forall a b. (a -> b) -> a -> b
$ RW -> Answer RW
forall (m :: * -> *) a. Monad m => a -> m a
return RW
initRW

-- | Add a new proposition to an existing collection.
assert :: Prop -> PropSet -> PropSet
assert :: Prop -> PropSet -> PropSet
assert Prop
p (State Answer RW
rws) = Answer RW -> PropSet
State (Answer RW -> PropSet) -> Answer RW -> PropSet
forall a b. (a -> b) -> a -> b
$ (((), RW) -> RW) -> Answer ((), RW) -> Answer RW
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), RW) -> RW
forall a b. (a, b) -> b
snd (Answer ((), RW) -> Answer RW) -> Answer ((), RW) -> Answer RW
forall a b. (a -> b) -> a -> b
$ RW -> Answer ((), RW)
m (RW -> Answer ((), RW)) -> Answer RW -> Answer ((), RW)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Answer RW
rws
  where S RW -> Answer ((), RW)
m = Prop -> S ()
prop 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 :: PropSet -> Maybe [(Int, Integer)]
checkSat (State Answer RW
m) = Answer RW -> Maybe [(Int, Integer)]
forall (m :: * -> *).
MonadPlus m =>
Answer RW -> m [(Int, Integer)]
go Answer RW
m
  where
  go :: Answer RW -> m [(Int, Integer)]
go Answer RW
None           = m [(Int, Integer)]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  go (One RW
rw)       = [(Int, Integer)] -> m [(Int, Integer)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Int
x,Integer
v) | (UserName Int
x, Integer
v) <- Inerts -> [(Name, Integer)]
iModel (RW -> Inerts
inerts RW
rw) ]
  go (Choice Answer RW
m1 Answer RW
m2) = m [(Int, Integer)] -> m [(Int, Integer)] -> m [(Int, Integer)]
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (Answer RW -> m [(Int, Integer)]
go Answer RW
m1) (Answer RW -> m [(Int, Integer)]
go Answer RW
m2)

allInerts :: PropSet -> [Inerts]
allInerts :: PropSet -> [Inerts]
allInerts (State Answer RW
m) = (RW -> Inerts) -> [RW] -> [Inerts]
forall a b. (a -> b) -> [a] -> [b]
map RW -> Inerts
inerts (Answer RW -> [RW]
forall a. Answer a -> [a]
toList Answer RW
m)

allSolutions :: PropSet -> [Solutions]
allSolutions :: PropSet -> [Solutions]
allSolutions = (Inerts -> Solutions) -> [Inerts] -> [Solutions]
forall a b. (a -> b) -> [a] -> [b]
map Inerts -> Solutions
startIter ([Inerts] -> [Solutions])
-> (PropSet -> [Inerts]) -> PropSet -> [Solutions]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropSet -> [Inerts]
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 :: BoundType -> Expr -> PropSet -> Maybe Integer
getExprBound BoundType
bt Expr
e (State Answer RW
s) =
  do let S RW -> Answer (Term, RW)
m          = Expr -> S Term
expr Expr
e
         check :: (Term, RW) -> Maybe Integer
check (Term
t,RW
s1) = BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt Term
t (RW -> Inerts
inerts RW
s1)
     [Integer]
bs <- ((Term, RW) -> Maybe Integer) -> [(Term, RW)] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, RW) -> Maybe Integer
check ([(Term, RW)] -> Maybe [Integer])
-> [(Term, RW)] -> Maybe [Integer]
forall a b. (a -> b) -> a -> b
$ Answer (Term, RW) -> [(Term, RW)]
forall a. Answer a -> [a]
toList (Answer (Term, RW) -> [(Term, RW)])
-> Answer (Term, RW) -> [(Term, RW)]
forall a b. (a -> b) -> a -> b
$ Answer RW
s Answer RW -> (RW -> Answer (Term, RW)) -> Answer (Term, RW)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RW -> Answer (Term, RW)
m
     case [Integer]
bs of
       [] -> Maybe Integer
forall a. Maybe a
Nothing
       [Integer]
_  -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
bs)

-- | Compute the range of possible values for an expression.
-- Returns `Nothing` if the bound is not known.
getExprRange :: Expr -> PropSet -> Maybe [Integer]
getExprRange :: Expr -> PropSet -> Maybe [Integer]
getExprRange Expr
e (State Answer RW
s) =
  do let S RW -> Answer (Term, RW)
m          = Expr -> S Term
expr Expr
e
         check :: (Term, RW) -> Maybe (Integer, Integer)
check (Term
t,RW
s1) = do Integer
l <- BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
Lower Term
t (RW -> Inerts
inerts RW
s1)
                           Integer
u <- BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
Upper Term
t (RW -> Inerts
inerts RW
s1)
                           (Integer, Integer) -> Maybe (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
l,Integer
u)
     [(Integer, Integer)]
bs <- ((Term, RW) -> Maybe (Integer, Integer))
-> [(Term, RW)] -> Maybe [(Integer, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, RW) -> Maybe (Integer, Integer)
check ([(Term, RW)] -> Maybe [(Integer, Integer)])
-> [(Term, RW)] -> Maybe [(Integer, Integer)]
forall a b. (a -> b) -> a -> b
$ Answer (Term, RW) -> [(Term, RW)]
forall a. Answer a -> [a]
toList (Answer (Term, RW) -> [(Term, RW)])
-> Answer (Term, RW) -> [(Term, RW)]
forall a b. (a -> b) -> a -> b
$ Answer RW
s Answer RW -> (RW -> Answer (Term, RW)) -> Answer (Term, RW)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RW -> Answer (Term, RW)
m
     case [(Integer, Integer)]
bs of
       [] -> Maybe [Integer]
forall a. Maybe a
Nothing
       [(Integer, Integer)]
_  -> let ([Integer]
ls,[Integer]
us) = [(Integer, Integer)] -> ([Integer], [Integer])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Integer, Integer)]
bs
             in [Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just [ Integer
x | Integer
x <- [ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
ls .. [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
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 (ReadPrec [Prop]
ReadPrec Prop
Int -> ReadS Prop
ReadS [Prop]
(Int -> ReadS Prop)
-> ReadS [Prop] -> ReadPrec Prop -> ReadPrec [Prop] -> Read Prop
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Prop]
$creadListPrec :: ReadPrec [Prop]
readPrec :: ReadPrec Prop
$creadPrec :: ReadPrec Prop
readList :: ReadS [Prop]
$creadList :: ReadS [Prop]
readsPrec :: Int -> ReadS Prop
$creadsPrec :: Int -> ReadS Prop
Read,Int -> Prop -> ShowS
[Prop] -> ShowS
Prop -> String
(Int -> Prop -> ShowS)
-> (Prop -> String) -> ([Prop] -> ShowS) -> Show Prop
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prop] -> ShowS
$cshowList :: [Prop] -> ShowS
show :: Prop -> String
$cshow :: Prop -> String
showsPrec :: Int -> Prop -> ShowS
$cshowsPrec :: Int -> Prop -> ShowS
Show,Eq Prop
Eq Prop
-> (Prop -> Prop -> Ordering)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Prop)
-> (Prop -> Prop -> Prop)
-> Ord Prop
Prop -> Prop -> Bool
Prop -> Prop -> Ordering
Prop -> Prop -> Prop
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Prop -> Prop -> Prop
$cmin :: Prop -> Prop -> Prop
max :: Prop -> Prop -> Prop
$cmax :: Prop -> Prop -> Prop
>= :: Prop -> Prop -> Bool
$c>= :: Prop -> Prop -> Bool
> :: Prop -> Prop -> Bool
$c> :: Prop -> Prop -> Bool
<= :: Prop -> Prop -> Bool
$c<= :: Prop -> Prop -> Bool
< :: Prop -> Prop -> Bool
$c< :: Prop -> Prop -> Bool
compare :: Prop -> Prop -> Ordering
$ccompare :: Prop -> Prop -> Ordering
$cp1Ord :: Eq Prop
Ord, Prop -> Prop -> Bool
(Prop -> Prop -> Bool) -> (Prop -> Prop -> Bool) -> Eq Prop
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prop -> Prop -> Bool
$c/= :: Prop -> Prop -> Bool
== :: Prop -> Prop -> Bool
$c== :: Prop -> Prop -> Bool
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 (ReadPrec [Expr]
ReadPrec Expr
Int -> ReadS Expr
ReadS [Expr]
(Int -> ReadS Expr)
-> ReadS [Expr] -> ReadPrec Expr -> ReadPrec [Expr] -> Read Expr
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Expr]
$creadListPrec :: ReadPrec [Expr]
readPrec :: ReadPrec Expr
$creadPrec :: ReadPrec Expr
readList :: ReadS [Expr]
$creadList :: ReadS [Expr]
readsPrec :: Int -> ReadS Expr
$creadsPrec :: Int -> ReadS Expr
Read,Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, Eq Expr
Eq Expr
-> (Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Expr)
-> (Expr -> Expr -> Expr)
-> Ord Expr
Expr -> Expr -> Bool
Expr -> Expr -> Ordering
Expr -> Expr -> Expr
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$c>= :: Expr -> Expr -> Bool
> :: Expr -> Expr -> Bool
$c> :: Expr -> Expr -> Bool
<= :: Expr -> Expr -> Bool
$c<= :: Expr -> Expr -> Bool
< :: Expr -> Expr -> Bool
$c< :: Expr -> Expr -> Bool
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
$cp1Ord :: Eq Expr
Ord, Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq)

prop :: Prop -> S ()
prop :: Prop -> S ()
prop Prop
PTrue       = () -> S ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
prop Prop
PFalse      = S ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
prop (Prop
p1 :|| Prop
p2) = Prop -> S ()
prop Prop
p1 S () -> S () -> S ()
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Prop -> S ()
prop Prop
p2
prop (Prop
p1 :&& Prop
p2) = Prop -> S ()
prop Prop
p1 S () -> S () -> S ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Prop -> S ()
prop Prop
p2
prop (Not Prop
p)     = Prop -> S ()
prop (Prop -> Prop
neg Prop
p)
  where
  neg :: Prop -> Prop
neg Prop
PTrue       = Prop
PFalse
  neg Prop
PFalse      = Prop
PTrue
  neg (Prop
p1 :&& Prop
p2) = Prop -> Prop
neg Prop
p1 Prop -> Prop -> Prop
:|| Prop -> Prop
neg Prop
p2
  neg (Prop
p1 :|| Prop
p2) = Prop -> Prop
neg Prop
p1 Prop -> Prop -> Prop
:&& Prop -> Prop
neg Prop
p2
  neg (Not Prop
q)     = Prop
q
  neg (Expr
e1 :== Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:/= Expr
e2
  neg (Expr
e1 :/= Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:== Expr
e2
  neg (Expr
e1 :<  Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:>= Expr
e2
  neg (Expr
e1 :<= Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:>  Expr
e2
  neg (Expr
e1 :>  Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:<= Expr
e2
  neg (Expr
e1 :>= Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:<  Expr
e2

prop (Expr
e1 :== Expr
e2) = do Term
t1 <- Expr -> S Term
expr Expr
e1
                      Term
t2 <- Expr -> S Term
expr Expr
e2
                      Term -> S ()
solveIs0 (Term
t1 Term -> Term -> Term
|-| Term
t2)

prop (Expr
e1 :/= Expr
e2)  = do Term
t1 <- Expr -> S Term
expr Expr
e1
                       Term
t2 <- Expr -> S Term
expr Expr
e2
                       let t :: Term
t = Term
t1 Term -> Term -> Term
|-| Term
t2
                       Term -> S ()
solveIsNeg Term
t S () -> S () -> S ()
`orElse` Term -> S ()
solveIsNeg (Term -> Term
tNeg Term
t)

prop (Expr
e1 :< Expr
e2)   = do Term
t1 <- Expr -> S Term
expr Expr
e1
                       Term
t2 <- Expr -> S Term
expr Expr
e2
                       Term -> S ()
solveIsNeg (Term
t1 Term -> Term -> Term
|-| Term
t2)

prop (Expr
e1 :<= Expr
e2)  = do Term
t1 <- Expr -> S Term
expr Expr
e1
                       Term
t2 <- Expr -> S Term
expr Expr
e2
                       let t :: Term
t = Term
t1 Term -> Term -> Term
|-| Term
t2 Term -> Term -> Term
|-| Integer -> Term
tConst Integer
1
                       Term -> S ()
solveIsNeg Term
t

prop (Expr
e1 :> Expr
e2)   = Prop -> S ()
prop (Expr
e2 Expr -> Expr -> Prop
:<  Expr
e1)
prop (Expr
e1 :>= Expr
e2)  = Prop -> S ()
prop (Expr
e2 Expr -> Expr -> Prop
:<= Expr
e1)


expr :: Expr -> S Term
expr :: Expr -> S Term
expr (Expr
e1 :+ Expr
e2)   = Term -> Term -> Term
(|+|)   (Term -> Term -> Term) -> S Term -> S (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e1 S (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> S Term
expr Expr
e2
expr (Expr
e1 :- Expr
e2)   = Term -> Term -> Term
(|-|)   (Term -> Term -> Term) -> S Term -> S (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e1 S (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> S Term
expr Expr
e2
expr (Integer
k  :* Expr
e2)   = (Integer
k Integer -> Term -> Term
|*|) (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e2
expr (Negate Expr
e)   = Term -> Term
tNeg    (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e
expr (Var Name
x)      = Term -> S Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Term
tVar Name
x)
expr (K Integer
x)        = Term -> S Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Term
tConst Integer
x)
expr (If Prop
p Expr
e1 Expr
e2) = do Name
x <- S Name
newVar
                       Prop -> S ()
prop (Prop
p Prop -> Prop -> Prop
:&& Name -> Expr
Var Name
x Expr -> Expr -> Prop
:== Expr
e1 Prop -> Prop -> Prop
:|| Prop -> Prop
Not Prop
p Prop -> Prop -> Prop
:&& Name -> Expr
Var Name
x Expr -> Expr -> Prop
:== Expr
e2)
                       Term -> S Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Term
tVar Name
x)
expr (Div Expr
e Integer
k)    = ((Term, Term) -> Term) -> S (Term, Term) -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> a
fst (S (Term, Term) -> S Term) -> S (Term, Term) -> S Term
forall a b. (a -> b) -> a -> b
$ Expr -> Integer -> S (Term, Term)
exprDivMod Expr
e Integer
k
expr (Mod Expr
e Integer
k)    = ((Term, Term) -> Term) -> S (Term, Term) -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> b
snd (S (Term, Term) -> S Term) -> S (Term, Term) -> S Term
forall a b. (a -> b) -> a -> b
$ Expr -> Integer -> S (Term, Term)
exprDivMod Expr
e Integer
k

exprDivMod :: Expr -> Integer -> S (Term,Term)
exprDivMod :: Expr -> Integer -> S (Term, Term)
exprDivMod Expr
e Integer
k =
  do Bool -> S ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) -- Always unsat
     Name
q <- S Name
newVar
     Name
r <- S Name
newVar
     let er :: Expr
er = Name -> Expr
Var Name
r
     Prop -> S ()
prop (Integer
k Integer -> Expr -> Expr
:* Name -> Expr
Var Name
q Expr -> Expr -> Expr
:+ Expr
er Expr -> Expr -> Prop
:== Expr
e Prop -> Prop -> Prop
:&& Expr
er Expr -> Expr -> Prop
:< Integer -> Expr
K Integer
k Prop -> Prop -> Prop
:&& Integer -> Expr
K Integer
0 Expr -> Expr -> Prop
:<= Expr
er)
     (Term, Term) -> S (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Term
tVar Name
q, Name -> Term
tVar Name
r)





--------------------------------------------------------------------------------

data RW = RW { RW -> Int
nameSource :: !Int
             , RW -> Inerts
inerts     :: Inerts
             } deriving Int -> RW -> ShowS
[RW] -> ShowS
RW -> String
(Int -> RW -> ShowS)
-> (RW -> String) -> ([RW] -> ShowS) -> Show RW
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RW] -> ShowS
$cshowList :: [RW] -> ShowS
show :: RW -> String
$cshow :: RW -> String
showsPrec :: Int -> RW -> ShowS
$cshowsPrec :: Int -> RW -> ShowS
Show

initRW :: RW
initRW :: RW
initRW = RW :: Int -> Inerts -> RW
RW { nameSource :: Int
nameSource = Int
0, inerts :: Inerts
inerts = Inerts
iNone }

--------------------------------------------------------------------------------
-- Constraints and Bound on Variables

ctLt :: Term -> Term -> Term
ctLt :: Term -> Term -> Term
ctLt Term
t1 Term
t2 = Term
t1 Term -> Term -> Term
|-| Term
t2

ctEq :: Term -> Term -> Term
ctEq :: Term -> Term -> Term
ctEq Term
t1 Term
t2 = Term
t1 Term -> Term -> Term
|-| Term
t2

data Bound      = Bound Integer Term  -- ^ The integer is strictly positive
                  deriving Int -> Bound -> ShowS
[Bound] -> ShowS
Bound -> String
(Int -> Bound -> ShowS)
-> (Bound -> String) -> ([Bound] -> ShowS) -> Show Bound
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Bound] -> ShowS
$cshowList :: [Bound] -> ShowS
show :: Bound -> String
$cshow :: Bound -> String
showsPrec :: Int -> Bound -> ShowS
$cshowsPrec :: Int -> Bound -> ShowS
Show

data BoundType  = Lower | Upper
                  deriving Int -> BoundType -> ShowS
[BoundType] -> ShowS
BoundType -> String
(Int -> BoundType -> ShowS)
-> (BoundType -> String)
-> ([BoundType] -> ShowS)
-> Show BoundType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BoundType] -> ShowS
$cshowList :: [BoundType] -> ShowS
show :: BoundType -> String
$cshow :: BoundType -> String
showsPrec :: Int -> BoundType -> ShowS
$cshowsPrec :: Int -> BoundType -> ShowS
Show

toCt :: BoundType -> Name -> Bound -> Term
toCt :: BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
x (Bound Integer
c Term
t) = Term -> Term -> Term
ctLt Term
t              (Integer
c Integer -> Term -> Term
|*| Name -> Term
tVar Name
x)
toCt BoundType
Upper Name
x (Bound Integer
c Term
t) = Term -> Term -> Term
ctLt (Integer
c Integer -> Term -> Term
|*| Name -> Term
tVar Name
x) Term
t



--------------------------------------------------------------------------------
-- Inert set

-- | The inert contains the solver state on one possible path.
data Inerts = Inerts
  { Inerts -> NameMap ([Bound], [Bound])
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@

  , Inerts -> NameMap Term
solved :: NameMap Term
    -- ^ Definitions for resolved variables.
    -- These form an idempotent substitution.
  } deriving Int -> Inerts -> ShowS
[Inerts] -> ShowS
Inerts -> String
(Int -> Inerts -> ShowS)
-> (Inerts -> String) -> ([Inerts] -> ShowS) -> Show Inerts
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Inerts] -> ShowS
$cshowList :: [Inerts] -> ShowS
show :: Inerts -> String
$cshow :: Inerts -> String
showsPrec :: Int -> Inerts -> ShowS
$cshowsPrec :: Int -> Inerts -> ShowS
Show

ppInerts :: Inerts -> Doc
ppInerts :: Inerts -> Doc
ppInerts Inerts
is = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [ Name -> Bound -> Doc
ppLower Name
x Bound
b | (Name
x,([Bound]
ls,[Bound]
_)) <- [(Name, ([Bound], [Bound]))]
bnds, Bound
b <- [Bound]
ls ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                     [ Name -> Bound -> Doc
ppUpper Name
x Bound
b | (Name
x,([Bound]
_,[Bound]
us)) <- [(Name, ([Bound], [Bound]))]
bnds, Bound
b <- [Bound]
us ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                     [ (Name, Term) -> Doc
ppEq (Name, Term)
e      | (Name, Term)
e <- NameMap Term -> [(Name, Term)]
forall k a. Map k a -> [(k, a)]
Map.toList (Inerts -> NameMap Term
solved Inerts
is) ]
  where
  bnds :: [(Name, ([Bound], [Bound]))]
bnds = NameMap ([Bound], [Bound]) -> [(Name, ([Bound], [Bound]))]
forall k a. Map k a -> [(k, a)]
Map.toList (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is)

  ppT :: Integer -> Name -> Doc
ppT Integer
c Name
x                = Term -> Doc
ppTerm (Integer
c Integer -> Term -> Term
|*| Name -> Term
tVar Name
x)
  ppLower :: Name -> Bound -> Doc
ppLower Name
x (Bound Integer
c Term
t)  = Term -> Doc
ppTerm Term
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"<" Doc -> Doc -> Doc
<+> Integer -> Name -> Doc
ppT Integer
c Name
x
  ppUpper :: Name -> Bound -> Doc
ppUpper Name
x (Bound Integer
c Term
t)  = Integer -> Name -> Doc
ppT Integer
c Name
x  Doc -> Doc -> Doc
<+> String -> Doc
text String
"<" Doc -> Doc -> Doc
<+> Term -> Doc
ppTerm Term
t
  ppEq :: (Name, Term) -> Doc
ppEq (Name
x,Term
t)             = Name -> Doc
ppName Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> Term -> Doc
ppTerm Term
t



-- | An empty inert set.
iNone :: Inerts
iNone :: Inerts
iNone = Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
Inerts { bounds :: NameMap ([Bound], [Bound])
bounds = NameMap ([Bound], [Bound])
forall k a. Map k a
Map.empty
               , solved :: NameMap Term
solved = NameMap Term
forall k a. Map k a
Map.empty
               }

-- | Rewrite a term using the definitions from an inert set.
iApSubst :: Inerts -> Term -> Term
iApSubst :: Inerts -> Term -> Term
iApSubst Inerts
i Term
t = ((Name, Term) -> Term -> Term) -> Term -> [(Name, Term)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, Term) -> Term -> Term
apS Term
t ([(Name, Term)] -> Term) -> [(Name, Term)] -> Term
forall a b. (a -> b) -> a -> b
$ NameMap Term -> [(Name, Term)]
forall k a. Map k a -> [(k, a)]
Map.toList (NameMap Term -> [(Name, Term)]) -> NameMap Term -> [(Name, Term)]
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap Term
solved Inerts
i
  where apS :: (Name, Term) -> Term -> Term
apS (Name
x,Term
t1) Term
t2 = Name -> Term -> Term -> Term
tLet Name
x Term
t1 Term
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 :: Name -> Term -> Inerts -> ([Term], Inerts)
iSolved Name
x Term
t Inerts
i =
  ( [Term]
kickedOut
  , Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
Inerts { bounds :: NameMap ([Bound], [Bound])
bounds = NameMap ([Bound], [Bound])
otherBounds
           , solved :: NameMap Term
solved = Name -> Term -> NameMap Term -> NameMap Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Term
t (NameMap Term -> NameMap Term) -> NameMap Term -> NameMap Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> NameMap Term -> NameMap Term
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Name -> Term -> Term -> Term
tLet Name
x Term
t) (NameMap Term -> NameMap Term) -> NameMap Term -> NameMap Term
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap Term
solved Inerts
i
           }
  )
  where
  ([Term]
kickedOut, NameMap ([Bound], [Bound])
otherBounds) =

        -- First, we eliminate all entries for `x`
    let (Maybe ([Bound], [Bound])
mb, NameMap ([Bound], [Bound])
mp1) = (Name -> ([Bound], [Bound]) -> Maybe ([Bound], [Bound]))
-> Name
-> NameMap ([Bound], [Bound])
-> (Maybe ([Bound], [Bound]), NameMap ([Bound], [Bound]))
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\Name
_ ([Bound], [Bound])
_ -> Maybe ([Bound], [Bound])
forall a. Maybe a
Nothing) Name
x (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
i)

        -- Next, we elminate all constraints that mentiond `x` in bounds
        mp2 :: Map Name (([Bound], [Bound]), [Term])
mp2 = (Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term]))
-> NameMap ([Bound], [Bound])
-> Map Name (([Bound], [Bound]), [Term])
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term])
extractBounds NameMap ([Bound], [Bound])
mp1

    in ( [ Term
ct | ([Bound]
lbs,[Bound]
ubs) <- Maybe ([Bound], [Bound]) -> [([Bound], [Bound])]
forall a. Maybe a -> [a]
maybeToList Maybe ([Bound], [Bound])
mb
              ,  Term
ct <- (Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
x) [Bound]
lbs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ (Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Upper Name
x) [Bound]
ubs ]
         [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++
         [ Term
ct | (([Bound], [Bound])
_,[Term]
cts) <- Map Name (([Bound], [Bound]), [Term])
-> [(([Bound], [Bound]), [Term])]
forall k a. Map k a -> [a]
Map.elems Map Name (([Bound], [Bound]), [Term])
mp2, Term
ct <- [Term]
cts ]

       , ((([Bound], [Bound]), [Term]) -> ([Bound], [Bound]))
-> Map Name (([Bound], [Bound]), [Term])
-> NameMap ([Bound], [Bound])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Bound], [Bound]), [Term]) -> ([Bound], [Bound])
forall a b. (a, b) -> a
fst Map Name (([Bound], [Bound]), [Term])
mp2
       )

  extractBounds :: Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term])
extractBounds Name
y ([Bound]
lbs,[Bound]
ubs) =
    let ([Bound]
lbsStay, [Bound]
lbsKick) = (Bound -> Bool) -> [Bound] -> ([Bound], [Bound])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Bound -> Bool
stay [Bound]
lbs
        ([Bound]
ubsStay, [Bound]
ubsKick) = (Bound -> Bool) -> [Bound] -> ([Bound], [Bound])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Bound -> Bool
stay [Bound]
ubs
    in ( ([Bound]
lbsStay,[Bound]
ubsStay)
       , (Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
y) [Bound]
lbsKick [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++
         (Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Upper Name
y) [Bound]
ubsKick
       )

  stay :: Bound -> Bool
stay (Bound Integer
_ Term
bnd) = Bool -> Bool
not (Name -> Term -> Bool
tHasVar Name
x Term
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 :: [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
boundInterval [Bound]
lbs [Bound]
ubs =
  do [Integer]
ls <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BoundType -> Bound -> Maybe Integer
normBound BoundType
Lower) [Bound]
lbs
     [Integer]
us <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BoundType -> Bound -> Maybe Integer
normBound BoundType
Upper) [Bound]
ubs
     let lb :: Maybe Integer
lb = case [Integer]
ls of
                [] -> Maybe Integer
forall a. Maybe a
Nothing
                [Integer]
_  -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
ls Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
         ub :: Maybe Integer
ub = case [Integer]
us of
                [] -> Maybe Integer
forall a. Maybe a
Nothing
                [Integer]
_  -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
us Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
     case (Maybe Integer
lb,Maybe Integer
ub) of
       (Just Integer
l, Just Integer
u) -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
u)
       (Maybe Integer, Maybe Integer)
_                -> () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     (Maybe Integer, Maybe Integer)
-> Maybe (Maybe Integer, Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
lb,Maybe Integer
ub)
  where
  normBound :: BoundType -> Bound -> Maybe Integer
normBound BoundType
Lower (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
                                   Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer
c)
  normBound BoundType
Upper (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
                                   Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
k Integer
c)

data Solutions = Done
               | TopVar Name Integer (Maybe Integer) (Maybe Integer) Inerts
               | FixedVar Name Integer Solutions
                  deriving Int -> Solutions -> ShowS
[Solutions] -> ShowS
Solutions -> String
(Int -> Solutions -> ShowS)
-> (Solutions -> String)
-> ([Solutions] -> ShowS)
-> Show Solutions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Solutions] -> ShowS
$cshowList :: [Solutions] -> ShowS
show :: Solutions -> String
$cshow :: Solutions -> String
showsPrec :: Int -> Solutions -> ShowS
$cshowsPrec :: Int -> Solutions -> ShowS
Show

slnCurrent :: Solutions -> [(Int,Integer)]
slnCurrent :: Solutions -> [(Int, Integer)]
slnCurrent Solutions
s = [ (Int
x,Integer
v) | (UserName Int
x, Integer
v) <- Solutions -> [(Name, Integer)]
go Solutions
s ]
  where
  go :: Solutions -> [(Name, Integer)]
go Solutions
Done                = []
  go (TopVar Name
x Integer
v Maybe Integer
_ Maybe Integer
_ Inerts
is) = (Name
x, Integer
v) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: Inerts -> [(Name, Integer)]
iModel (Name -> Integer -> Inerts -> Inerts
iLet Name
x Integer
v Inerts
is)
  go (FixedVar Name
x Integer
v Solutions
i)    = (Name
x, Integer
v) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: Solutions -> [(Name, Integer)]
go Solutions
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 :: Name -> Integer -> Inerts -> Inerts
iLet Name
x Integer
v Inerts
is = Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
Inerts { bounds :: NameMap ([Bound], [Bound])
bounds = (([Bound], [Bound]) -> ([Bound], [Bound]))
-> NameMap ([Bound], [Bound]) -> NameMap ([Bound], [Bound])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Bound], [Bound]) -> ([Bound], [Bound])
updBs (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is)
                     , solved :: NameMap Term
solved = (Term -> Term) -> NameMap Term -> NameMap Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Integer -> Term -> Term
tLetNum Name
x Integer
v) (Inerts -> NameMap Term
solved Inerts
is) }
  where
  updB :: Bound -> Bound
updB (Bound Integer
c Term
t) = Integer -> Term -> Bound
Bound Integer
c (Name -> Integer -> Term -> Term
tLetNum Name
x Integer
v Term
t)
  updBs :: ([Bound], [Bound]) -> ([Bound], [Bound])
updBs ([Bound]
ls,[Bound]
us)    = ((Bound -> Bound) -> [Bound] -> [Bound]
forall a b. (a -> b) -> [a] -> [b]
map Bound -> Bound
updB [Bound]
ls, (Bound -> Bound) -> [Bound] -> [Bound]
forall a b. (a -> b) -> [a] -> [b]
map Bound -> Bound
updB [Bound]
us)


startIter :: Inerts -> Solutions
startIter :: Inerts -> Solutions
startIter Inerts
is =
  case NameMap ([Bound], [Bound])
-> Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is) of
    Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
Nothing ->
      case NameMap Term -> Maybe ((Name, Term), NameMap Term)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey (Inerts -> NameMap Term
solved Inerts
is) of
        Maybe ((Name, Term), NameMap Term)
Nothing -> Solutions
Done
        Just ((Name
x,Term
t), NameMap Term
mp1) ->
          case [ Name
y | Name
y <- Term -> [Name]
tVarList Term
t ] of
            Name
y : [Name]
_ -> Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
y Integer
0 Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing Inerts
is
            [] -> let v :: Integer
v = Term -> Integer
tConstPart Term
t
                  in Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
x Integer
v (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
v) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
v) (Inerts -> Solutions) -> Inerts -> Solutions
forall a b. (a -> b) -> a -> b
$ Inerts
is { solved :: NameMap Term
solved = NameMap Term
mp1 }
    Just ((Name
x,([Bound]
lbs,[Bound]
ubs)), NameMap ([Bound], [Bound])
mp1) ->
      case [ Name
y | Bound Integer
_ Term
t <- [Bound]
lbs [Bound] -> [Bound] -> [Bound]
forall a. [a] -> [a] -> [a]
++ [Bound]
ubs, Name
y <- Term -> [Name]
tVarList Term
t ] of
        Name
y : [Name]
_ -> Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
y Integer
0 Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing Inerts
is
        [] -> case [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
boundInterval [Bound]
lbs [Bound]
ubs of
                Maybe (Maybe Integer, Maybe Integer)
Nothing -> String -> Solutions
forall a. HasCallStack => String -> a
error String
"bug: cannot compute interval?"
                Just (Maybe Integer
lb,Maybe Integer
ub) ->
                  let v :: Integer
v = Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe Integer
0 (Maybe Integer -> Maybe Integer -> Maybe Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus Maybe Integer
lb Maybe Integer
ub)
                  in Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
x Integer
v Maybe Integer
lb Maybe Integer
ub (Inerts -> Solutions) -> Inerts -> Solutions
forall a b. (a -> b) -> a -> b
$ Inerts
is { bounds :: NameMap ([Bound], [Bound])
bounds = NameMap ([Bound], [Bound])
mp1 }

slnEnumerate :: Solutions -> [ Solutions ]
slnEnumerate :: Solutions -> [Solutions]
slnEnumerate Solutions
s0 = Solutions -> [Solutions] -> [Solutions]
go Solutions
s0 []
  where
  go :: Solutions -> [Solutions] -> [Solutions]
go Solutions
s [Solutions]
k  = case Solutions -> Maybe Solutions
slnNextVar Solutions
s of
              Maybe Solutions
Nothing -> Solutions -> [Solutions] -> [Solutions]
hor Solutions
s [Solutions]
k
              Just Solutions
s1 -> Solutions -> [Solutions] -> [Solutions]
go Solutions
s1 ([Solutions] -> [Solutions]) -> [Solutions] -> [Solutions]
forall a b. (a -> b) -> a -> b
$ case Solutions -> Maybe Solutions
slnNextVal Solutions
s of
                                   Maybe Solutions
Nothing -> [Solutions]
k
                                   Just Solutions
s2 -> Solutions -> [Solutions] -> [Solutions]
go Solutions
s2 [Solutions]
k

  hor :: Solutions -> [Solutions] -> [Solutions]
hor Solutions
s [Solutions]
k = Solutions
s
          Solutions -> [Solutions] -> [Solutions]
forall a. a -> [a] -> [a]
: case Solutions -> Maybe Solutions
slnNextVal Solutions
s of
              Maybe Solutions
Nothing -> [Solutions]
k
              Just Solutions
s1 -> Solutions -> [Solutions] -> [Solutions]
hor Solutions
s1 [Solutions]
k

slnNextVal :: Solutions -> Maybe Solutions
slnNextVal :: Solutions -> Maybe Solutions
slnNextVal Solutions
Done = Maybe Solutions
forall a. Maybe a
Nothing
slnNextVal (FixedVar Name
x Integer
v Solutions
i) = Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Solutions -> Maybe Solutions
slnNextVal Solutions
i
slnNextVal it :: Solutions
it@(TopVar Name
_ Integer
_ Maybe Integer
lb Maybe Integer
_ Inerts
_) =
  case Maybe Integer
lb of
    Just Integer
_  -> (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Solutions
it
    Maybe Integer
Nothing -> (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract Integer
1) Solutions
it


slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith Integer -> Integer
_ Solutions
Done = Maybe Solutions
forall a. Maybe a
Nothing
slnNextValWith Integer -> Integer
f (FixedVar Name
x Integer
v Solutions
i) = Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith Integer -> Integer
f Solutions
i
slnNextValWith Integer -> Integer
f (TopVar Name
x Integer
v Maybe Integer
lb Maybe Integer
ub Inerts
is) =
  do let v1 :: Integer
v1 = Integer -> Integer
f Integer
v
     case Maybe Integer
lb of
       Just Integer
l  -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
v1)
       Maybe Integer
Nothing -> () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     case Maybe Integer
ub of
       Just Integer
u  -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
v1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
u)
       Maybe Integer
Nothing -> () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     Solutions -> Maybe Solutions
forall (m :: * -> *) a. Monad m => a -> m a
return (Solutions -> Maybe Solutions) -> Solutions -> Maybe Solutions
forall a b. (a -> b) -> a -> b
$ Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
x Integer
v1 Maybe Integer
lb Maybe Integer
ub Inerts
is

slnNextVar :: Solutions -> Maybe Solutions
slnNextVar :: Solutions -> Maybe Solutions
slnNextVar Solutions
Done                = Maybe Solutions
forall a. Maybe a
Nothing
slnNextVar (TopVar Name
x Integer
v Maybe Integer
_ Maybe Integer
_ Inerts
is) = Solutions -> Maybe Solutions
forall a. a -> Maybe a
Just (Solutions -> Maybe Solutions) -> Solutions -> Maybe Solutions
forall a b. (a -> b) -> a -> b
$ Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Solutions -> Solutions
forall a b. (a -> b) -> a -> b
$ Inerts -> Solutions
startIter (Inerts -> Solutions) -> Inerts -> Solutions
forall a b. (a -> b) -> a -> b
$ Name -> Integer -> Inerts -> Inerts
iLet Name
x Integer
v Inerts
is
slnNextVar (FixedVar Name
x Integer
v Solutions
i)    = Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Solutions -> Maybe Solutions
slnNextVar Solutions
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 :: BoundType -> [Bound] -> Maybe Integer
iPickBounded BoundType
_ [] = Maybe Integer
forall a. Maybe a
Nothing
iPickBounded BoundType
bt [Bound]
bs =
  do [Integer]
xs <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BoundType -> Bound -> Maybe Integer
normBound BoundType
bt) [Bound]
bs
     Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ case BoundType
bt of
                BoundType
Lower -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
xs
                BoundType
Upper -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
xs
  where
  -- t < c*x
  -- <=> t+1 <= c*x
  -- <=> (t+1)/c <= x
  -- <=> ceil((t+1)/c) <= x
  -- <=> t `div` c + 1 <= x
  normBound :: BoundType -> Bound -> Maybe Integer
normBound BoundType
Lower (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
                                   Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
k Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
  -- c*x < t
  -- <=> c*x <= t-1
  -- <=> x   <= (t-1)/c
  -- <=> x   <= floor((t-1)/c)
  -- <=> x   <= (t-1) `div` c
  normBound BoundType
Upper (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
                                   Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
kInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) Integer
c)


-- | The largest (resp. least) upper (resp. lower) bound on a term
-- that will satisfy the model
iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt (T Integer
k NameMap Integer
xs) Inerts
is = do [Integer]
ks <- ((Name, Integer) -> Maybe Integer)
-> [(Name, Integer)] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Integer) -> Maybe Integer
summand (NameMap Integer -> [(Name, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
xs)
                               Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
k Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
ks
  where
  summand :: (Name, Integer) -> Maybe Integer
summand (Name
x,Integer
c) = (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) (BoundType -> Name -> Inerts -> Maybe Integer
iVarBound (Integer -> BoundType
forall a. (Ord a, Num a) => a -> BoundType
newBt Integer
c) Name
x Inerts
is)
  newBt :: a -> BoundType
newBt a
c = if a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 then BoundType
bt else case BoundType
bt of
                                    BoundType
Lower -> BoundType
Upper
                                    BoundType
Upper -> BoundType
Lower


-- | The largest (resp. least) upper (resp. lower) bound on a variable
-- that will satisfy the model.
iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
iVarBound BoundType
bt Name
x Inerts
is
  | Just Term
t <- Name -> NameMap Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Inerts -> NameMap Term
solved Inerts
is) = BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt Term
t Inerts
is

iVarBound BoundType
bt Name
x Inerts
is =
  do ([Bound], [Bound])
both <- Name -> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is)
     case (Bound -> Maybe Integer) -> [Bound] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Bound -> Maybe Integer
fromBound (([Bound], [Bound]) -> [Bound]
forall b. (b, b) -> b
chooseBounds ([Bound], [Bound])
both) of
       [] -> Maybe Integer
forall a. Maybe a
Nothing
       [Integer]
bs -> Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return ([Integer] -> Integer
combineBounds [Integer]
bs)
  where
  fromBound :: Bound -> Maybe Integer
fromBound (Bound Integer
c Term
t) = (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
scaleBound Integer
c) (BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt Term
t Inerts
is)

  combineBounds :: [Integer] -> Integer
combineBounds = case BoundType
bt of
                    BoundType
Upper -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum
                    BoundType
Lower -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum

  chooseBounds :: (b, b) -> b
chooseBounds = case BoundType
bt of
                   BoundType
Upper -> (b, b) -> b
forall a b. (a, b) -> b
snd
                   BoundType
Lower -> (b, b) -> b
forall a b. (a, b) -> a
fst

  scaleBound :: a -> a -> a
scaleBound a
c a
b = case BoundType
bt of
                     BoundType
Upper -> a -> a -> a
forall a. Integral a => a -> a -> a
div (a
ba -> a -> a
forall a. Num a => a -> a -> a
-a
1) a
c
                     BoundType
Lower -> a -> a -> a
forall a. Integral a => a -> a -> a
div a
b a
c a -> a -> a
forall a. Num a => a -> a -> a
+ a
1




iModel :: Inerts -> [(Name,Integer)]
iModel :: Inerts -> [(Name, Integer)]
iModel Inerts
i = [(Name, Integer)]
-> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
goBounds [] (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
i)
  where
  goBounds :: [(Name, Integer)]
-> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
goBounds [(Name, Integer)]
su NameMap ([Bound], [Bound])
mp =
    case NameMap ([Bound], [Bound])
-> Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey NameMap ([Bound], [Bound])
mp of
      Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
Nothing -> [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
goEqs [(Name, Integer)]
su ([(Name, Term)] -> [(Name, Integer)])
-> [(Name, Term)] -> [(Name, Integer)]
forall a b. (a -> b) -> a -> b
$ NameMap Term -> [(Name, Term)]
forall k a. Map k a -> [(k, a)]
Map.toList (NameMap Term -> [(Name, Term)]) -> NameMap Term -> [(Name, Term)]
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap Term
solved Inerts
i
      Just ((Name
x,([Bound]
lbs0,[Bound]
ubs0)), NameMap ([Bound], [Bound])
mp1) ->
        let lbs :: [Bound]
lbs = [ Integer -> Term -> Bound
Bound Integer
c ([(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
su Term
t) | Bound Integer
c Term
t <- [Bound]
lbs0 ]
            ubs :: [Bound]
ubs = [ Integer -> Term -> Bound
Bound Integer
c ([(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
su Term
t) | Bound Integer
c Term
t <- [Bound]
ubs0 ]
            sln :: Integer
sln = Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe Integer
0
                (Maybe Integer -> Integer) -> Maybe Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Maybe Integer -> Maybe Integer -> Maybe Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (BoundType -> [Bound] -> Maybe Integer
iPickBounded BoundType
Lower [Bound]
lbs) (BoundType -> [Bound] -> Maybe Integer
iPickBounded BoundType
Upper [Bound]
ubs)
        in [(Name, Integer)]
-> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
goBounds ((Name
x,Integer
sln) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: [(Name, Integer)]
su) NameMap ([Bound], [Bound])
mp1

  goEqs :: [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
goEqs [(Name, Integer)]
su [] = [(Name, Integer)]
su
  goEqs [(Name, Integer)]
su ((Name
x,Term
t) : [(Name, Term)]
more) =
    let t1 :: Term
t1  = [(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
su Term
t
        vs :: [Name]
vs  = Term -> [Name]
tVarList Term
t1
        su1 :: [(Name, Integer)]
su1 = [ (Name
v,Integer
0) | Name
v <- [Name]
vs ] [(Name, Integer)] -> [(Name, Integer)] -> [(Name, Integer)]
forall a. [a] -> [a] -> [a]
++ (Name
x,Term -> Integer
tConstPart Term
t1) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: [(Name, Integer)]
su
    in [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
goEqs [(Name, Integer)]
su1 [(Name, Term)]
more


--------------------------------------------------------------------------------
-- Solving constraints

solveIs0 :: Term -> S ()
solveIs0 :: Term -> S ()
solveIs0 Term
t = Term -> S ()
solveIs0' (Term -> S ()) -> S Term -> S ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> S Term
apSubst Term
t

-- | Solve a constraint if the form @t = 0@.
-- Assumes substitution has already been applied.
solveIs0' :: Term -> S ()
solveIs0' :: Term -> S ()
solveIs0' Term
t

  -- A == 0
  | Just Integer
a <- Term -> Maybe Integer
isConst Term
t = Bool -> S ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)

  -- A + B * x = 0
  | Just (Integer
a,Integer
b,Name
x) <- Term -> Maybe (Integer, Integer, Name)
tIsOneVar Term
t =
    case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (-Integer
a) Integer
b of
      (Integer
q,Integer
0) -> Name -> Term -> S ()
addDef Name
x (Integer -> Term
tConst Integer
q)
      (Integer, Integer)
_     -> S ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero

  --  x + S = 0
  -- -x + S = 0
  | Just (Integer
xc,Name
x,Term
s) <- Term -> Maybe (Integer, Name, Term)
tGetSimpleCoeff Term
t =
    Name -> Term -> S ()
addDef Name
x (if Integer
xc Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Term -> Term
tNeg Term
s else Term
s)

  -- A * S = 0
  | Just (Integer
_, Term
s) <- Term -> Maybe (Integer, Term)
tFactor Term
t  = Term -> S ()
solveIs0 Term
s

  -- See Section 3.1 of paper for details.
  -- We obtain an equivalent formulation but with smaller coefficients.
  | Just (Integer
ak,Name
xk,Term
s) <- Term -> Maybe (Integer, Name, Term)
tLeastAbsCoeff Term
t =
      do let m :: Integer
m = Integer -> Integer
forall a. Num a => a -> a
abs Integer
ak Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
         Name
v <- S Name
newVar
         let sgn :: Integer
sgn  = Integer -> Integer
forall a. Num a => a -> a
signum Integer
ak
             soln :: Term
soln =     (Integer -> Integer
forall a. Num a => a -> a
negate Integer
sgn Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Integer -> Term -> Term
|*| Name -> Term
tVar Name
v
                    Term -> Term -> Term
|+| (Integer -> Integer) -> Term -> Term
tMapCoeff (\Integer
c -> Integer
sgn Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer -> Integer -> Integer
modulus Integer
c Integer
m) Term
s
         Name -> Term -> S ()
addDef Name
xk Term
soln

         let upd :: Integer -> Integer
upd Integer
i = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) (Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
m) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
modulus Integer
i Integer
m
         Term -> S ()
solveIs0 (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer
forall a. Num a => a -> a
abs Integer
ak) Integer -> Term -> Term
|*| Name -> Term
tVar Name
v Term -> Term -> Term
|+| (Integer -> Integer) -> Term -> Term
tMapCoeff Integer -> Integer
upd Term
s)

  | Bool
otherwise = String -> S ()
forall a. HasCallStack => String -> a
error String
"solveIs0: unreachable"

modulus :: Integer -> Integer -> Integer
modulus :: Integer -> Integer -> Integer
modulus Integer
a Integer
m = Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m)


solveIsNeg :: Term -> S ()
solveIsNeg :: Term -> S ()
solveIsNeg Term
t = Term -> S ()
solveIsNeg' (Term -> S ()) -> S Term -> S ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> S Term
apSubst Term
t


-- | Solve a constraint of the form @t < 0@.
-- Assumes that substitution has been applied
solveIsNeg' :: Term -> S ()
solveIsNeg' :: Term -> S ()
solveIsNeg' Term
t

  -- A < 0
  | Just Integer
a <- Term -> Maybe Integer
isConst Term
t = Bool -> S ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)

  -- A * S < 0
  | Just (Integer
_,Term
s) <- Term -> Maybe (Integer, Term)
tFactor Term
t = Term -> S ()
solveIsNeg Term
s

  -- See Section 5.1 of the paper
  | Just (Integer
xc,Name
x,Term
s) <- Term -> Maybe (Integer, Name, Term)
tLeastVar Term
t =

    do [(Integer, Term, Integer, Term)]
ctrs <- if Integer
xc Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
               -- -XC*x + S < 0
               -- S < XC*x
               then do [Bound]
ubs <- BoundType -> Name -> S [Bound]
getBounds BoundType
Upper Name
x
                       let b :: Integer
b    = Integer -> Integer
forall a. Num a => a -> a
negate Integer
xc
                           beta :: Term
beta = Term
s
                       BoundType -> Name -> Bound -> S ()
addBound BoundType
Lower Name
x (Integer -> Term -> Bound
Bound Integer
b Term
beta)
                       [(Integer, Term, Integer, Term)]
-> S [(Integer, Term, Integer, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Integer
a,Term
alpha,Integer
b,Term
beta) | Bound Integer
a Term
alpha <- [Bound]
ubs ]
               -- XC*x + S < 0
               -- XC*x < -S
               else do [Bound]
lbs <- BoundType -> Name -> S [Bound]
getBounds BoundType
Lower Name
x
                       let a :: Integer
a     = Integer
xc
                           alpha :: Term
alpha = Term -> Term
tNeg Term
s
                       BoundType -> Name -> Bound -> S ()
addBound BoundType
Upper Name
x (Integer -> Term -> Bound
Bound Integer
a Term
alpha)
                       [(Integer, Term, Integer, Term)]
-> S [(Integer, Term, Integer, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Integer
a,Term
alpha,Integer
b,Term
beta) | Bound Integer
b Term
beta <- [Bound]
lbs ]

      -- See Note [Shadows]
       ((Integer, Term, Integer, Term) -> S ())
-> [(Integer, Term, Integer, Term)] -> S ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Integer
a,Term
alpha,Integer
b,Term
beta) ->
          do let real :: Term
real = Term -> Term -> Term
ctLt (Integer
a Integer -> Term -> Term
|*| Term
beta) (Integer
b Integer -> Term -> Term
|*| Term
alpha)
                 dark :: Term
dark = Term -> Term -> Term
ctLt (Integer -> Term
tConst (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b)) (Integer
b Integer -> Term -> Term
|*| Term
alpha Term -> Term -> Term
|-| Integer
a Integer -> Term -> Term
|*| Term
beta)
                 gray :: [Term]
gray = [ Term -> Term -> Term
ctEq (Integer
b Integer -> Term -> Term
|*| Name -> Term
tVar Name
x) (Integer -> Term
tConst Integer
i Term -> Term -> Term
|+| Term
beta)
                                                      | Integer
i <- [ Integer
1 .. Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 ] ]
             Term -> S ()
solveIsNeg Term
real
             (S () -> S () -> S ()) -> S () -> [S ()] -> S ()
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl S () -> S () -> S ()
orElse (Term -> S ()
solveIsNeg Term
dark) ((Term -> S ()) -> [Term] -> [S ()]
forall a b. (a -> b) -> [a] -> [b]
map Term -> S ()
solveIs0 [Term]
gray)
             ) [(Integer, Term, Integer, Term)]
ctrs

  | Bool
otherwise = String -> S ()
forall a. HasCallStack => String -> a
error String
"solveIsNeg: unreachable"

orElse :: S () -> S () -> S ()
orElse :: S () -> S () -> S ()
orElse S ()
x S ()
y = S () -> S () -> S ()
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus S ()
x S ()
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 Int -> Answer a -> ShowS
[Answer a] -> ShowS
Answer a -> String
(Int -> Answer a -> ShowS)
-> (Answer a -> String) -> ([Answer a] -> ShowS) -> Show (Answer a)
forall a. Show a => Int -> Answer a -> ShowS
forall a. Show a => [Answer a] -> ShowS
forall a. Show a => Answer a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Answer a] -> ShowS
$cshowList :: forall a. Show a => [Answer a] -> ShowS
show :: Answer a -> String
$cshow :: forall a. Show a => Answer a -> String
showsPrec :: Int -> Answer a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Answer a -> ShowS
Show


answerSize :: Answer a -> (Integer,Integer,Integer)
answerSize :: Answer a -> (Integer, Integer, Integer)
answerSize = Integer
-> Integer -> Integer -> Answer a -> (Integer, Integer, Integer)
forall t t t a.
(Num t, Num t, Num t) =>
t -> t -> t -> Answer a -> (t, t, t)
go Integer
0 Integer
0 Integer
0
  where
  go :: t -> t -> t -> Answer a -> (t, t, t)
go !t
n !t
o !t
c Answer a
ans =
    case Answer a
ans of
      Answer a
None  -> (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1, t
o, t
c)
      One a
_ -> (t
n, t
o t -> t -> t
forall a. Num a => a -> a -> a
+ t
1, t
c)
      Choice Answer a
x Answer a
y ->
        case t -> t -> t -> Answer a -> (t, t, t)
go t
n t
o (t
ct -> t -> t
forall a. Num a => a -> a -> a
+t
1) Answer a
x of
          (t
n',t
o',t
c') -> t -> t -> t -> Answer a -> (t, t, t)
go t
n' t
o' t
c' Answer a
y


dotAnswer :: (a -> Doc) -> Answer a -> Doc
dotAnswer :: (a -> Doc) -> Answer a -> Doc
dotAnswer a -> Doc
pp Answer a
g0 = [Doc] -> Doc
vcat [String -> Doc
text String
"digraph {", Int -> Doc -> Doc
nest Int
2 ((Doc, Integer) -> Doc
forall a b. (a, b) -> a
fst ((Doc, Integer) -> Doc) -> (Doc, Integer) -> Doc
forall a b. (a -> b) -> a -> b
$ Integer -> Answer a -> (Doc, Integer)
go Integer
0 Answer a
g0), String -> Doc
text String
"}"]
  where
  node :: Integer -> a -> Doc
node Integer
x a
d            = Integer -> Doc
integer Integer
x Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (String -> Doc
text String
"label=" Doc -> Doc -> Doc
<> String -> Doc
text (a -> String
forall a. Show a => a -> String
show a
d))
                                                              Doc -> Doc -> Doc
<> Doc
semi
  edge :: Integer -> Integer -> Doc
edge Integer
x Integer
y            = Integer -> Doc
integer Integer
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
y

  go :: Integer -> Answer a -> (Doc, Integer)
go Integer
x Answer a
None           = let x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
                        in Integer -> (Doc, Integer) -> (Doc, Integer)
seq Integer
x' ( Integer -> String -> Doc
forall a. Show a => Integer -> a -> Doc
node Integer
x String
"", Integer
x' )
  go Integer
x (One a
a)        = let x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
                        in Integer -> (Doc, Integer) -> (Doc, Integer)
seq Integer
x' ( Integer -> String -> Doc
forall a. Show a => Integer -> a -> Doc
node Integer
x (Doc -> String
forall a. Show a => a -> String
show (a -> Doc
pp a
a)), Integer
x' )
  go Integer
x (Choice Answer a
c1 Answer a
c2) = let x' :: Integer
x'       = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
                            (Doc
ls1,Integer
x1) = Integer -> Answer a -> (Doc, Integer)
go Integer
x' Answer a
c1
                            (Doc
ls2,Integer
x2) = Integer -> Answer a -> (Doc, Integer)
go Integer
x1    Answer a
c2
                        in Integer -> (Doc, Integer) -> (Doc, Integer)
seq Integer
x'
                           ( [Doc] -> Doc
vcat [ Integer -> String -> Doc
forall a. Show a => Integer -> a -> Doc
node Integer
x String
"|"
                                  , Integer -> Integer -> Doc
edge Integer
x Integer
x'
                                  , Integer -> Integer -> Doc
edge Integer
x Integer
x1
                                  , Doc
ls1
                                  , Doc
ls2
                                  ], Integer
x2 )
toList :: Answer a -> [a]
toList :: Answer a -> [a]
toList Answer a
a = Answer a -> [a] -> [a]
forall a. Answer a -> [a] -> [a]
go Answer a
a []
  where
  go :: Answer a -> [a] -> [a]
go (Choice Answer a
xs Answer a
ys) [a]
zs = Answer a -> [a] -> [a]
go Answer a
xs (Answer a -> [a] -> [a]
go Answer a
ys [a]
zs)
  go (One a
x) [a]
xs        = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs
  go Answer a
None [a]
xs           = [a]
xs


instance Monad Answer where
  return :: a -> Answer a
return a
a           = a -> Answer a
forall a. a -> Answer a
One a
a
#if !MIN_VERSION_ghc(8,8,1)
  fail _             = None
#endif
  Answer a
None >>= :: Answer a -> (a -> Answer b) -> Answer b
>>= a -> Answer b
_         = Answer b
forall a. Answer a
None
  One a
a >>= a -> Answer b
k        = a -> Answer b
k a
a
  Choice Answer a
m1 Answer a
m2 >>= a -> Answer b
k = Answer b -> Answer b -> Answer b
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (Answer a
m1 Answer a -> (a -> Answer b) -> Answer b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Answer b
k) (Answer a
m2 Answer a -> (a -> Answer b) -> Answer b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Answer b
k)

instance Alternative Answer where
  empty :: Answer a
empty = Answer a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  <|> :: Answer a -> Answer a -> Answer a
(<|>) = Answer a -> Answer a -> Answer a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus

instance MonadPlus Answer where
  mzero :: Answer a
mzero                = Answer a
forall a. Answer a
None
  mplus :: Answer a -> Answer a -> Answer a
mplus Answer a
None Answer a
x = Answer a
x
  -- mplus (Choice x y) z = mplus x (mplus y z)
  mplus Answer a
x Answer a
y    = Answer a -> Answer a -> Answer a
forall a. Answer a -> Answer a -> Answer a
Choice Answer a
x Answer a
y

instance Functor Answer where
  fmap :: (a -> b) -> Answer a -> Answer b
fmap a -> b
_ Answer a
None           = Answer b
forall a. Answer a
None
  fmap a -> b
f (One a
x)        = b -> Answer b
forall a. a -> Answer a
One (a -> b
f a
x)
  fmap a -> b
f (Choice Answer a
x1 Answer a
x2) = Answer b -> Answer b -> Answer b
forall a. Answer a -> Answer a -> Answer a
Choice ((a -> b) -> Answer a -> Answer b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Answer a
x1) ((a -> b) -> Answer a -> Answer b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Answer a
x2)

instance Applicative Answer where
  pure :: a -> Answer a
pure  = a -> Answer a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Answer (a -> b) -> Answer a -> Answer b
(<*>) = Answer (a -> b) -> Answer a -> Answer b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap


newtype S a = S (RW -> Answer (a,RW))

instance Monad S where
  return :: a -> S a
return a
a      = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
s -> (a, RW) -> Answer (a, RW)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a,RW
s)
  S RW -> Answer (a, RW)
m >>= :: S a -> (a -> S b) -> S b
>>= a -> S b
k     = (RW -> Answer (b, RW)) -> S b
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (b, RW)) -> S b) -> (RW -> Answer (b, RW)) -> S b
forall a b. (a -> b) -> a -> b
$ \RW
s -> do (a
a,RW
s1) <- RW -> Answer (a, RW)
m RW
s
                               let S RW -> Answer (b, RW)
m1 = a -> S b
k a
a
                               RW -> Answer (b, RW)
m1 RW
s1

instance Alternative S where
  empty :: S a
empty = S a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  <|> :: S a -> S a -> S a
(<|>) = S a -> S a -> S a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus

instance MonadPlus S where
  mzero :: S a
mzero               = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
_ -> Answer (a, RW)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  mplus :: S a -> S a -> S a
mplus (S RW -> Answer (a, RW)
m1) (S RW -> Answer (a, RW)
m2) = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
s -> Answer (a, RW) -> Answer (a, RW) -> Answer (a, RW)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (RW -> Answer (a, RW)
m1 RW
s) (RW -> Answer (a, RW)
m2 RW
s)

instance Functor S where
  fmap :: (a -> b) -> S a -> S b
fmap = (a -> b) -> S a -> S b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative S where
  pure :: a -> S a
pure  = a -> S a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: S (a -> b) -> S a -> S b
(<*>) = S (a -> b) -> S a -> S b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

updS :: (RW -> (a,RW)) -> S a
updS :: (RW -> (a, RW)) -> S a
updS RW -> (a, RW)
f = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
s -> (a, RW) -> Answer (a, RW)
forall (m :: * -> *) a. Monad m => a -> m a
return (RW -> (a, RW)
f RW
s)

updS_ :: (RW -> RW) -> S ()
updS_ :: (RW -> RW) -> S ()
updS_ RW -> RW
f = (RW -> ((), RW)) -> S ()
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> ((), RW)) -> S ()) -> (RW -> ((), RW)) -> S ()
forall a b. (a -> b) -> a -> b
$ \RW
rw -> ((),RW -> RW
f RW
rw)

get :: (RW -> a) -> S a
get :: (RW -> a) -> S a
get RW -> a
f = (RW -> (a, RW)) -> S a
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> (a, RW)) -> S a) -> (RW -> (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
rw -> (RW -> a
f RW
rw, RW
rw)

newVar :: S Name
newVar :: S Name
newVar = (RW -> (Name, RW)) -> S Name
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> (Name, RW)) -> S Name) -> (RW -> (Name, RW)) -> S Name
forall a b. (a -> b) -> a -> b
$ \RW
rw -> ( Int -> Name
SysName (RW -> Int
nameSource RW
rw)
                       , RW
rw { nameSource :: Int
nameSource = RW -> Int
nameSource RW
rw Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
                       )

-- | Get lower ('fst'), or upper ('snd') bounds for a variable.
getBounds :: BoundType -> Name -> S [Bound]
getBounds :: BoundType -> Name -> S [Bound]
getBounds BoundType
f Name
x = (RW -> [Bound]) -> S [Bound]
forall a. (RW -> a) -> S a
get ((RW -> [Bound]) -> S [Bound]) -> (RW -> [Bound]) -> S [Bound]
forall a b. (a -> b) -> a -> b
$ \RW
rw -> case Name -> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound]))
-> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap ([Bound], [Bound])
bounds (Inerts -> NameMap ([Bound], [Bound]))
-> Inerts -> NameMap ([Bound], [Bound])
forall a b. (a -> b) -> a -> b
$ RW -> Inerts
inerts RW
rw of
                               Maybe ([Bound], [Bound])
Nothing -> []
                               Just ([Bound], [Bound])
bs -> case BoundType
f of
                                            BoundType
Lower -> ([Bound], [Bound]) -> [Bound]
forall a b. (a, b) -> a
fst ([Bound], [Bound])
bs
                                            BoundType
Upper -> ([Bound], [Bound]) -> [Bound]
forall a b. (a, b) -> b
snd ([Bound], [Bound])
bs

addBound :: BoundType -> Name -> Bound -> S ()
addBound :: BoundType -> Name -> Bound -> S ()
addBound BoundType
bt Name
x Bound
b = (RW -> RW) -> S ()
updS_ ((RW -> RW) -> S ()) -> (RW -> RW) -> S ()
forall a b. (a -> b) -> a -> b
$ \RW
rw ->
  let i :: Inerts
i = RW -> Inerts
inerts RW
rw
      entry :: ([Bound], [Bound])
entry = case BoundType
bt of
                BoundType
Lower -> ([Bound
b],[])
                BoundType
Upper -> ([],[Bound
b])
      jn :: ([a], [a]) -> ([a], [a]) -> ([a], [a])
jn ([a]
newL,[a]
newU) ([a]
oldL,[a]
oldU) = ([a]
newL[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
oldL, [a]
newU[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
oldU)
  in RW
rw { inerts :: Inerts
inerts = Inerts
i { bounds :: NameMap ([Bound], [Bound])
bounds = (([Bound], [Bound]) -> ([Bound], [Bound]) -> ([Bound], [Bound]))
-> Name
-> ([Bound], [Bound])
-> NameMap ([Bound], [Bound])
-> NameMap ([Bound], [Bound])
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ([Bound], [Bound]) -> ([Bound], [Bound]) -> ([Bound], [Bound])
forall a a. ([a], [a]) -> ([a], [a]) -> ([a], [a])
jn Name
x ([Bound], [Bound])
entry (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
i) }}

-- | Add a new definition.
-- Assumes substitution has already been applied
addDef :: Name -> Term -> S ()
addDef :: Name -> Term -> S ()
addDef Name
x Term
t =
  do [Term]
newWork <- (RW -> ([Term], RW)) -> S [Term]
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> ([Term], RW)) -> S [Term])
-> (RW -> ([Term], RW)) -> S [Term]
forall a b. (a -> b) -> a -> b
$ \RW
rw -> let ([Term]
newWork,Inerts
newInerts) = Name -> Term -> Inerts -> ([Term], Inerts)
iSolved Name
x Term
t (RW -> Inerts
inerts RW
rw)
                              in ([Term]
newWork, RW
rw { inerts :: Inerts
inerts = Inerts
newInerts })
     (Term -> S ()) -> [Term] -> S ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Term -> S ()
solveIsNeg [Term]
newWork

apSubst :: Term -> S Term
apSubst :: Term -> S Term
apSubst Term
t =
  do Inerts
i <- (RW -> Inerts) -> S Inerts
forall a. (RW -> a) -> S a
get RW -> Inerts
inerts
     Term -> S Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Inerts -> Term -> Term
iApSubst Inerts
i Term
t)




--------------------------------------------------------------------------------


data Name = UserName !Int | SysName !Int
            deriving (ReadPrec [Name]
ReadPrec Name
Int -> ReadS Name
ReadS [Name]
(Int -> ReadS Name)
-> ReadS [Name] -> ReadPrec Name -> ReadPrec [Name] -> Read Name
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Name]
$creadListPrec :: ReadPrec [Name]
readPrec :: ReadPrec Name
$creadPrec :: ReadPrec Name
readList :: ReadS [Name]
$creadList :: ReadS [Name]
readsPrec :: Int -> ReadS Name
$creadsPrec :: Int -> ReadS Name
Read,Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show,Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq,Eq Name
Eq Name
-> (Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord)

ppName :: Name -> Doc
ppName :: Name -> Doc
ppName (UserName Int
x) = String -> Doc
text String
"u" Doc -> Doc -> Doc
<> Int -> Doc
int Int
x
ppName (SysName Int
x)  = String -> Doc
text String
"s" Doc -> Doc -> Doc
<> Int -> Doc
int Int
x

toName :: Int -> Name
toName :: Int -> Name
toName = Int -> Name
UserName

fromName :: Name -> Maybe Int
fromName :: Name -> Maybe Int
fromName (UserName Int
x) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
x
fromName (SysName Int
_)  = Maybe Int
forall a. Maybe a
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 (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq,Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord)

infixl 6 |+|, |-|
infixr 7 |*|

-- | A constant term.
tConst :: Integer -> Term
tConst :: Integer -> Term
tConst Integer
k = Integer -> NameMap Integer -> Term
T Integer
k NameMap Integer
forall k a. Map k a
Map.empty

-- | Construct a term with a single variable.
tVar :: Name -> Term
tVar :: Name -> Term
tVar Name
x = Integer -> NameMap Integer -> Term
T Integer
0 (Name -> Integer -> NameMap Integer
forall k a. k -> a -> Map k a
Map.singleton Name
x Integer
1)

(|+|) :: Term -> Term -> Term
T Integer
n1 NameMap Integer
m1 |+| :: Term -> Term -> Term
|+| T Integer
n2 NameMap Integer
m2 = Integer -> NameMap Integer -> Term
T (Integer
n1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n2)
                    (NameMap Integer -> Term) -> NameMap Integer -> Term
forall a b. (a -> b) -> a -> b
$ if NameMap Integer -> Bool
forall k a. Map k a -> Bool
Map.null NameMap Integer
m1 then NameMap Integer
m2 else
                      if NameMap Integer -> Bool
forall k a. Map k a -> Bool
Map.null NameMap Integer
m2 then NameMap Integer
m1 else
                      (Integer -> Bool) -> NameMap Integer -> NameMap Integer
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) (NameMap Integer -> NameMap Integer)
-> NameMap Integer -> NameMap Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> NameMap Integer -> NameMap Integer -> NameMap Integer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) NameMap Integer
m1 NameMap Integer
m2

(|*|) :: Integer -> Term -> Term
Integer
0 |*| :: Integer -> Term -> Term
|*| Term
_     = Integer -> Term
tConst Integer
0
Integer
1 |*| Term
t     = Term
t
Integer
k |*| T Integer
n NameMap Integer
m = Integer -> NameMap Integer -> Term
T (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
n) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) NameMap Integer
m)

tNeg :: Term -> Term
tNeg :: Term -> Term
tNeg Term
t = (-Integer
1) Integer -> Term -> Term
|*| Term
t

(|-|) :: Term -> Term -> Term
Term
t1 |-| :: Term -> Term -> Term
|-| Term
t2 = Term
t1 Term -> Term -> Term
|+| Term -> Term
tNeg Term
t2


-- | Replace a variable with a term.
tLet :: Name -> Term -> Term -> Term
tLet :: Name -> Term -> Term -> Term
tLet Name
x Term
t1 Term
t2 = let (Integer
a,Term
t) = Name -> Term -> (Integer, Term)
tSplitVar Name
x Term
t2
               in Integer
a Integer -> Term -> Term
|*| Term
t1 Term -> Term -> Term
|+| Term
t

-- | Replace a variable with a constant.
tLetNum :: Name -> Integer -> Term -> Term
tLetNum :: Name -> Integer -> Term -> Term
tLetNum Name
x Integer
k Term
t = let (Integer
c,T Integer
n NameMap Integer
m) = Name -> Term -> (Integer, Term)
tSplitVar Name
x Term
t
                in Integer -> NameMap Integer -> Term
T (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) NameMap Integer
m

-- | Replace the given variables with constants.
tLetNums :: [(Name,Integer)] -> Term -> Term
tLetNums :: [(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
xs Term
t = ((Name, Integer) -> Term -> Term)
-> Term -> [(Name, Integer)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
x,Integer
i) Term
t1 -> Name -> Integer -> Term -> Term
tLetNum Name
x Integer
i Term
t1) Term
t [(Name, Integer)]
xs




instance Show Term where
  showsPrec :: Int -> Term -> ShowS
showsPrec Int
c Term
t = Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
c (Doc -> String
forall a. Show a => a -> String
show (Term -> Doc
ppTerm Term
t))

ppTerm :: Term -> Doc
ppTerm :: Term -> Doc
ppTerm (T Integer
k NameMap Integer
m) =
  case NameMap Integer -> [(Name, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
m of
    []              -> Integer -> Doc
integer Integer
k
    [(Name, Integer)]
xs     | Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 -> [Doc] -> Doc
hsep (Integer -> Doc
integer Integer
k Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Name, Integer) -> Doc) -> [(Name, Integer)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Integer) -> Doc
ppProd [(Name, Integer)]
xs)
    (Name, Integer)
x : [(Name, Integer)]
xs          -> [Doc] -> Doc
hsep ((Name, Integer) -> Doc
ppFst (Name, Integer)
x   Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Name, Integer) -> Doc) -> [(Name, Integer)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Integer) -> Doc
ppProd [(Name, Integer)]
xs)

  where
  ppFst :: (Name, Integer) -> Doc
ppFst (Name
x,Integer
1)  = Name -> Doc
ppName Name
x
  ppFst (Name
x,-1) = String -> Doc
text String
"-" Doc -> Doc -> Doc
<> Name -> Doc
ppName Name
x
  ppFst (Name
x,Integer
n)  = Integer -> Name -> Doc
ppMul Integer
n Name
x

  ppProd :: (Name, Integer) -> Doc
ppProd (Name
x,Integer
1)  = String -> Doc
text String
"+" Doc -> Doc -> Doc
<+> Name -> Doc
ppName Name
x
  ppProd (Name
x,-1) = String -> Doc
text String
"-" Doc -> Doc -> Doc
<+> Name -> Doc
ppName Name
x
  ppProd (Name
x,Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0      = String -> Doc
text String
"+" Doc -> Doc -> Doc
<+> Integer -> Name -> Doc
ppMul Integer
n Name
x
               | Bool
otherwise  = String -> Doc
text String
"-" Doc -> Doc -> Doc
<+> Integer -> Name -> Doc
ppMul (Integer -> Integer
forall a. Num a => a -> a
abs Integer
n) Name
x

  ppMul :: Integer -> Name -> Doc
ppMul Integer
n Name
x = Integer -> Doc
integer Integer
n Doc -> Doc -> Doc
<+> String -> Doc
text String
"*" Doc -> Doc -> Doc
<+> Name -> Doc
ppName Name
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 :: Name -> Term -> (Integer, Term)
tSplitVar Name
x t :: Term
t@(T Integer
n NameMap Integer
m) =
  case (Name -> Integer -> Maybe Integer)
-> Name -> NameMap Integer -> (Maybe Integer, NameMap Integer)
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\Name
_ Integer
_ -> Maybe Integer
forall a. Maybe a
Nothing) Name
x NameMap Integer
m of
    (Maybe Integer
Nothing,NameMap Integer
_) -> (Integer
0,Term
t)
    (Just Integer
k,NameMap Integer
m1) -> (Integer
k, Integer -> NameMap Integer -> Term
T Integer
n NameMap Integer
m1)

-- | Does the term contain this varibale?
tHasVar :: Name -> Term -> Bool
tHasVar :: Name -> Term -> Bool
tHasVar Name
x (T Integer
_ NameMap Integer
m) = Name -> NameMap Integer -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Name
x NameMap Integer
m

-- | Is this terms just an integer.
isConst :: Term -> Maybe Integer
isConst :: Term -> Maybe Integer
isConst (T Integer
n NameMap Integer
m)
  | NameMap Integer -> Bool
forall k a. Map k a -> Bool
Map.null NameMap Integer
m  = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
  | Bool
otherwise   = Maybe Integer
forall a. Maybe a
Nothing

tConstPart :: Term -> Integer
tConstPart :: Term -> Integer
tConstPart (T Integer
n NameMap Integer
_) = Integer
n

-- | Returns: @Just (a, b, x)@ if the term is the form: @a + b * x@
tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
tIsOneVar (T Integer
a NameMap Integer
m) = case NameMap Integer -> [(Name, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
m of
                      [ (Name
x,Integer
b) ] -> (Integer, Integer, Name) -> Maybe (Integer, Integer, Name)
forall a. a -> Maybe a
Just (Integer
a, Integer
b, Name
x)
                      [(Name, Integer)]
_         -> Maybe (Integer, Integer, Name)
forall a. Maybe a
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 :: Term -> Maybe (Integer, Name, Term)
tGetSimpleCoeff (T Integer
a NameMap Integer
m) =
  do let (NameMap Integer
m1,NameMap Integer
m2) = (Integer -> Bool)
-> NameMap Integer -> (NameMap Integer, NameMap Integer)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition (\Integer
x -> Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 Bool -> Bool -> Bool
|| Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -Integer
1) NameMap Integer
m
     ((Name
x,Integer
xc), NameMap Integer
m3) <- NameMap Integer -> Maybe ((Name, Integer), NameMap Integer)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey NameMap Integer
m1
     (Integer, Name, Term) -> Maybe (Integer, Name, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
xc, Name
x, Integer -> NameMap Integer -> Term
T Integer
a (NameMap Integer -> NameMap Integer -> NameMap Integer
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union NameMap Integer
m3 NameMap Integer
m2))

tVarList :: Term -> [Name]
tVarList :: Term -> [Name]
tVarList (T Integer
_ NameMap Integer
m) = NameMap Integer -> [Name]
forall k a. Map k a -> [k]
Map.keys NameMap Integer
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 :: Term -> Maybe (Integer, Term)
tFactor (T Integer
c NameMap Integer
m) =
  do Integer
d <- [Integer] -> Maybe Integer
common (Integer
c Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: NameMap Integer -> [Integer]
forall k a. Map k a -> [a]
Map.elems NameMap Integer
m)
     (Integer, Term) -> Maybe (Integer, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
d, Integer -> NameMap Integer -> Term
T (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
c Integer
d) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d) NameMap Integer
m))
  where
  common :: [Integer] -> Maybe Integer
  common :: [Integer] -> Maybe Integer
common []  = Maybe Integer
forall a. Maybe a
Nothing
  common [Integer
x] = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
x
  common (Integer
x : Integer
y : [Integer]
zs) =
    case Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
x Integer
y of
      Integer
1 -> Maybe Integer
forall a. Maybe a
Nothing
      Integer
n -> [Integer] -> Maybe Integer
common (Integer
n Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
zs)

-- | Extract a variable with a coefficient whose absolute value is minimal.
tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)
tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)
tLeastAbsCoeff (T Integer
c NameMap Integer
m) = do (Integer
xc,Name
x,NameMap Integer
m1) <- (Name
 -> Integer
 -> Maybe (Integer, Name, NameMap Integer)
 -> Maybe (Integer, Name, NameMap Integer))
-> Maybe (Integer, Name, NameMap Integer)
-> NameMap Integer
-> Maybe (Integer, Name, NameMap Integer)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Name
-> Integer
-> Maybe (Integer, Name, NameMap Integer)
-> Maybe (Integer, Name, NameMap Integer)
forall a.
(Ord a, Num a) =>
Name
-> a
-> Maybe (a, Name, NameMap Integer)
-> Maybe (a, Name, NameMap Integer)
step Maybe (Integer, Name, NameMap Integer)
forall a. Maybe a
Nothing NameMap Integer
m
                            (Integer, Name, Term) -> Maybe (Integer, Name, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
xc, Name
x, Integer -> NameMap Integer -> Term
T Integer
c NameMap Integer
m1)
  where
  step :: Name
-> a
-> Maybe (a, Name, NameMap Integer)
-> Maybe (a, Name, NameMap Integer)
step Name
x a
xc Maybe (a, Name, NameMap Integer)
Nothing   = (a, Name, NameMap Integer) -> Maybe (a, Name, NameMap Integer)
forall a. a -> Maybe a
Just (a
xc, Name
x, Name -> NameMap Integer -> NameMap Integer
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
x NameMap Integer
m)
  step Name
x a
xc (Just (a
yc,Name
_,NameMap Integer
_))
    | a -> a
forall a. Num a => a -> a
abs a
xc a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a -> a
forall a. Num a => a -> a
abs a
yc = (a, Name, NameMap Integer) -> Maybe (a, Name, NameMap Integer)
forall a. a -> Maybe a
Just (a
xc, Name
x, Name -> NameMap Integer -> NameMap Integer
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
x NameMap Integer
m)
  step Name
_ a
_ Maybe (a, Name, NameMap Integer)
it         = Maybe (a, Name, NameMap Integer)
it

-- | Extract the least variable from a term
tLeastVar :: Term -> Maybe (Integer, Name, Term)
tLeastVar :: Term -> Maybe (Integer, Name, Term)
tLeastVar (T Integer
c NameMap Integer
m) =
  do ((Name
x,Integer
xc), NameMap Integer
m1) <- NameMap Integer -> Maybe ((Name, Integer), NameMap Integer)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey NameMap Integer
m
     (Integer, Name, Term) -> Maybe (Integer, Name, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
xc, Name
x, Integer -> NameMap Integer -> Term
T Integer
c NameMap Integer
m1)

-- | Apply a function to all coefficients, including the constnat
tMapCoeff :: (Integer -> Integer) -> Term -> Term
tMapCoeff :: (Integer -> Integer) -> Term -> Term
tMapCoeff Integer -> Integer
f (T Integer
c NameMap Integer
m) = Integer -> NameMap Integer -> Term
T (Integer -> Integer
f Integer
c) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f NameMap Integer
m)