{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Safe #-}

{- |
This module implements a decision procedure for quantifier-free linear
arithmetic.  The algorithm is based on the following paper:

  An Online Proof-Producing Decision Procedure for
  Mixed-Integer Linear Arithmetic
  by
  Sergey Berezin, Vijay Ganesh, and David L. Dill
-}
module Data.Integer.SAT (
  PropSet,
  noProps,
  checkSat,
  assert,
  Prop (..),
  Expr (..),
  BoundType (..),
  getExprBound,
  getExprRange,
  Name,
  toName,
  fromName,

  -- * Iterators
  allSolutions,
  slnCurrent,
  slnNextVal,
  slnNextVar,
  slnEnumerate,

  -- * Debug
  dotPropSet,
  sizePropSet,
  allInerts,
  ppInerts,

  -- * For QuickCheck
  iPickBounded,
  Bound (..),
  tConst,
) where

import Control.Applicative (Alternative (..), Applicative (..), (<$>))
import Control.Monad (MonadPlus (..), ap, guard, liftM)
import Data.List (partition)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
import Text.PrettyPrint
import Prelude hiding ((<>))

infixr 2 :||

infixr 3 :&&

infix 4 :==, :/=, :<, :<=, :>, :>=

infixl 6 :+, :-

infixl 7 :*

--------------------------------------------------------------------------------
-- Solver interface

-- | A collection of propositions.
newtype PropSet = State (Answer RW)
  deriving (Int -> PropSet -> ShowS
[PropSet] -> ShowS
PropSet -> String
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) = forall a. (a -> Doc) -> Answer a -> Doc
dotAnswer (Inerts -> Doc
ppInerts 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) = 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ RW -> Answer ((), RW)
m 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) = forall {m :: * -> *}.
MonadPlus m =>
Answer RW -> m [(Int, Integer)]
go Answer RW
m
  where
    go :: Answer RW -> m [(Int, Integer)]
go Answer RW
None = forall (m :: * -> *) a. MonadPlus m => m a
mzero
    go (One RW
rw) = 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) = 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) = forall a b. (a -> b) -> [a] -> [b]
map RW -> Inerts
inerts (forall a. Answer a -> [a]
toList Answer RW
m)

allSolutions :: PropSet -> [Solutions]
allSolutions :: PropSet -> [Solutions]
allSolutions = forall a b. (a -> b) -> [a] -> [b]
map Inerts -> Solutions
startIter 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, RW) -> Maybe Integer
check forall a b. (a -> b) -> a -> b
$ forall a. Answer a -> [a]
toList forall a b. (a -> b) -> a -> b
$ Answer RW
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RW -> Answer (Term, RW)
m
    case [Integer]
bs of
      [] -> forall a. Maybe a
Nothing
      [Integer]
_ -> forall a. a -> Maybe a
Just (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)
          forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
l, Integer
u)
    [(Integer, Integer)]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, RW) -> Maybe (Integer, Integer)
check forall a b. (a -> b) -> a -> b
$ forall a. Answer a -> [a]
toList forall a b. (a -> b) -> a -> b
$ Answer RW
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RW -> Answer (Term, RW)
m
    case [(Integer, Integer)]
bs of
      [] -> forall a. Maybe a
Nothing
      [(Integer, Integer)]
_ ->
        let ([Integer]
ls, [Integer]
us) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Integer, Integer)]
bs
         in forall a. a -> Maybe a
Just [Integer
x | Integer
x <- [forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
ls .. 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]
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
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
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
Ord, Prop -> Prop -> Bool
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
  = -- | Addition
    Expr :+ Expr
  | -- | Subtraction
    Expr :- Expr
  | -- | Multiplication by a constant
    Integer :* Expr
  | -- | Negation
    Negate Expr
  | -- | Variable
    Var Name
  | -- | Constant
    K Integer
  | -- | A conditional expression
    If Prop Expr Expr
  | -- | Division, rounds down
    Div Expr Integer
  | -- | Non-negative remainder
    Mod Expr Integer
  | -- | Minimum of two arguments
    Min Expr Expr
  | -- | Maximum of two arguments
    Max Expr Expr
  deriving (ReadPrec [Expr]
ReadPrec Expr
Int -> ReadS Expr
ReadS [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
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
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
Ord, Expr -> Expr -> Bool
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 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
prop Prop
PFalse = forall (m :: * -> *) a. MonadPlus m => m a
mzero
prop (Prop
p1 :|| Prop
p2) = Prop -> S ()
prop Prop
p1 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 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
(|+|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e1 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
(|-|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e1 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
|*|) 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e
expr (Var Name
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Term
tVar Name
x)
expr (K Integer
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Term
tConst Integer
x)
expr (Min Expr
a Expr
b) = Expr -> S Term
expr (Prop -> Expr -> Expr -> Expr
If (Expr
a Expr -> Expr -> Prop
:<= Expr
b) Expr
a Expr
b)
expr (Max Expr
a Expr
b) = Expr -> S Term
expr (Prop -> Expr -> Expr -> Expr
If (Expr
a Expr -> Expr -> Prop
:<= Expr
b) Expr
b Expr
a)
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)
  forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Term
tVar Name
x)
expr (Div Expr
e Integer
k) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Expr -> Integer -> S (Term, Term)
exprDivMod Expr
e Integer
k
expr (Mod Expr
e Integer
k) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd 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
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
k 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)
    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
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 {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
  = -- | The integer is strictly positive
    Bound Integer Term
  deriving (Int -> Bound -> ShowS
[Bound] -> ShowS
Bound -> String
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
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
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 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]
      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]
      forall a. [a] -> [a] -> [a]
++ [(Name, Term) -> Doc
ppEq (Name, Term)
e | (Name, Term)
e <- forall k a. Map k a -> [(k, a)]
Map.toList (Inerts -> NameMap Term
solved Inerts
is)]
  where
    bnds :: [(Name, ([Bound], [Bound]))]
bnds = 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
    { bounds :: NameMap ([Bound], [Bound])
bounds = forall k a. Map k a
Map.empty
    , solved :: NameMap Term
solved = 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, Term) -> Term -> Term
apS Term
t forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList 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
      { bounds :: NameMap ([Bound], [Bound])
bounds = NameMap ([Bound], [Bound])
otherBounds
      , solved :: NameMap Term
solved = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Term
t forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Name -> Term -> Term -> Term
tLet Name
x Term
t) 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) = forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\Name
_ ([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 = 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) <- forall a. Maybe a -> [a]
maybeToList Maybe ([Bound], [Bound])
mb, Term
ct <- forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
x) [Bound]
lbs forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Upper Name
x) [Bound]
ubs
            ]
              forall a. [a] -> [a] -> [a]
++ [Term
ct | (([Bound], [Bound])
_, [Term]
cts) <- forall k a. Map k a -> [a]
Map.elems Map Name (([Bound], [Bound]), [Term])
mp2, Term
ct <- [Term]
cts]
          , forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Bound -> Bool
stay [Bound]
lbs
          ([Bound]
ubsStay, [Bound]
ubsKick) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Bound -> Bool
stay [Bound]
ubs
       in ( ([Bound]
lbsStay, [Bound]
ubsStay)
          , forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
y) [Bound]
lbsKick
              forall a. [a] -> [a] -> [a]
++ 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 <- 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 <- 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
          [] -> forall a. Maybe a
Nothing
          [Integer]
_ -> forall a. a -> Maybe a
Just (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
ls forall a. Num a => a -> a -> a
+ Integer
1)
        ub :: Maybe Integer
ub = case [Integer]
us of
          [] -> forall a. Maybe a
Nothing
          [Integer]
_ -> forall a. a -> Maybe a
Just (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
us forall a. Num a => a -> a -> a
- Integer
1)
    case (Maybe Integer
lb, Maybe Integer
ub) of
      (Just Integer
l, Just Integer
u) -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
l forall a. Ord a => a -> a -> Bool
<= Integer
u)
      (Maybe Integer, Maybe Integer)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    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
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Integral a => a -> a -> a
div (Integer
k forall a. Num a => a -> a -> a
+ Integer
c 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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
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) 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) 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
    { bounds :: NameMap ([Bound], [Bound])
bounds = 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 = 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) = (forall a b. (a -> b) -> [a] -> [b]
map Bound -> Bound
updB [Bound]
ls, forall a b. (a -> b) -> [a] -> [b]
map Bound -> Bound
updB [Bound]
us)

startIter :: Inerts -> Solutions
startIter :: Inerts -> Solutions
startIter Inerts
is =
  case 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 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 forall a. Maybe a
Nothing 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 (forall a. a -> Maybe a
Just Integer
v) (forall a. a -> Maybe a
Just Integer
v) 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 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 forall a. Maybe a
Nothing 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 -> forall a. HasCallStack => String -> a
error String
"bug: cannot compute interval?"
          Just (Maybe Integer
lb, Maybe Integer
ub) ->
            let v :: Integer
v = forall a. a -> Maybe a -> a
fromMaybe Integer
0 (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 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 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
        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 = forall a. Maybe a
Nothing
slnNextVal (FixedVar Name
x Integer
v Solutions
i) = Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v 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 (forall a. Num a => a -> a -> a
+ Integer
1) Solutions
it
    Maybe Integer
Nothing -> (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith (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 = 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 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 -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
l forall a. Ord a => a -> a -> Bool
<= Integer
v1)
      Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    case Maybe Integer
ub of
      Just Integer
u -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
v1 forall a. Ord a => a -> a -> Bool
<= Integer
u)
      Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a. Maybe a
Nothing
slnNextVar (TopVar Name
x Integer
v Maybe Integer
_ Maybe Integer
_ Inerts
is) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v forall a b. (a -> b) -> a -> b
$ Inerts -> Solutions
startIter 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 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
_ [] = forall a. Maybe a
Nothing
iPickBounded BoundType
bt [Bound]
bs =
  do
    [Integer]
xs <- 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
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case BoundType
bt of
      BoundType
Lower -> forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
xs
      BoundType
Upper -> 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
k forall a. Integral a => a -> a -> a
`div` Integer
c 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Integral a => a -> a -> a
div (Integer
k 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Integer) -> Maybe Integer
summand (forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
xs)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ Integer
k forall a. a -> [a] -> [a]
: [Integer]
ks
  where
    summand :: (Name, Integer) -> Maybe Integer
summand (Name
x, Integer
c) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer
c forall a. Num a => a -> a -> a
*) (BoundType -> Name -> Inerts -> Maybe Integer
iVarBound (forall {a}. (Ord a, Num a) => a -> BoundType
newBt Integer
c) Name
x Inerts
is)
    newBt :: a -> BoundType
newBt a
c =
      if a
c 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 <- 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 <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is)
    case forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Bound -> Maybe Integer
fromBound (forall {b}. (b, b) -> b
chooseBounds ([Bound], [Bound])
both) of
      [] -> forall a. Maybe a
Nothing
      [Integer]
bs -> 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) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 -> forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum
      BoundType
Lower -> forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum

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

    scaleBound :: a -> a -> a
scaleBound a
c a
b = case BoundType
bt of
      BoundType
Upper -> forall a. Integral a => a -> a -> a
div (a
b forall a. Num a => a -> a -> a
- a
1) a
c
      BoundType
Lower -> forall a. Integral a => a -> a -> a
div a
b a
c 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 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 forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList 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 =
                forall a. a -> Maybe a -> a
fromMaybe Integer
0 forall a b. (a -> b) -> a -> b
$
                  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) 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] forall a. [a] -> [a] -> [a]
++ (Name
x, Term -> Integer
tConstPart Term
t1) 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' 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 = forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
a 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 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)
_ -> 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 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 = forall a. Num a => a -> a
abs Integer
ak forall a. Num a => a -> a -> a
+ Integer
1
        Name
v <- S Name
newVar
        let sgn :: Integer
sgn = forall a. Num a => a -> a
signum Integer
ak
            soln :: Term
soln =
              (forall a. Num a => a -> a
negate Integer
sgn 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 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 = forall a. Integral a => a -> a -> a
div (Integer
2 forall a. Num a => a -> a -> a
* Integer
i forall a. Num a => a -> a -> a
+ Integer
m) (Integer
2 forall a. Num a => a -> a -> a
* Integer
m) forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
modulus Integer
i Integer
m
        Term -> S ()
solveIs0 (forall a. Num a => a -> a
negate (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 = forall a. HasCallStack => String -> a
error String
"solveIs0: unreachable"

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

solveIsNeg :: Term -> S ()
solveIsNeg :: Term -> S ()
solveIsNeg Term
t = Term -> S ()
solveIsNeg' 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 = forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
a 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 forall a. Ord a => a -> a -> Bool
< Integer
0
            then -- -XC*x + S < 0
            -- S < XC*x
            do
              [Bound]
ubs <- BoundType -> Name -> S [Bound]
getBounds BoundType
Upper Name
x
              let b :: Integer
b = 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)
              forall (m :: * -> *) a. Monad m => a -> m a
return [(Integer
a, Term
alpha, Integer
b, Term
beta) | Bound Integer
a Term
alpha <- [Bound]
ubs]
            else -- XC*x + S < 0
            -- XC*x < -S
            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)
              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]
        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 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 forall a. Num a => a -> a -> a
- Integer
1]
                      ]
                Term -> S ()
solveIsNeg Term
real
                forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl S () -> S () -> S ()
orElse (Term -> S ()
solveIsNeg Term
dark) (forall a b. (a -> b) -> [a] -> [b]
map Term -> S ()
solveIs0 [Term]
gray)
          )
          [(Integer, Term, Integer, Term)]
ctrs
  | Bool
otherwise = forall a. HasCallStack => String -> a
error String
"solveIsNeg: unreachable"

orElse :: S () -> S () -> S ()
orElse :: S () -> S () -> S ()
orElse S ()
x S ()
y = 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
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 :: forall a. Answer a -> (Integer, Integer, Integer)
answerSize = 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
n forall a. Num a => a -> a -> a
+ t
1, t
o, t
c)
        One a
_ -> (t
n, t
o 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
c 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 :: forall a. (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 (forall a b. (a, b) -> a
fst 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 (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 forall a. Num a => a -> a -> a
+ Integer
1
       in seq :: forall a b. a -> b -> b
seq Integer
x' (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 forall a. Num a => a -> a -> a
+ Integer
1
       in seq :: forall a b. a -> b -> b
seq Integer
x' (forall {a}. Show a => Integer -> a -> Doc
node Integer
x (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 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 seq :: forall a b. a -> b -> b
seq
            Integer
x'
            ( [Doc] -> Doc
vcat
                [ 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 :: forall a. Answer a -> [a]
toList Answer 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 forall a. a -> [a] -> [a]
: [a]
xs
    go Answer a
None [a]
xs = [a]
xs

instance Monad Answer where
  Answer a
None >>= :: forall a b. Answer a -> (a -> Answer b) -> Answer b
>>= a -> 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 = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (Answer a
m1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Answer b
k) (Answer a
m2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Answer b
k)

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

instance MonadPlus Answer where
  mzero :: forall a. Answer a
mzero = forall a. Answer a
None
  mplus :: forall a. 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 = forall a. Answer a -> Answer a -> Answer a
Choice Answer a
x Answer a
y

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

instance Applicative Answer where
  pure :: forall a. a -> Answer a
pure = forall a. a -> Answer a
One
  <*> :: forall a 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
  S RW -> Answer (a, RW)
m >>= :: forall a b. S a -> (a -> S b) -> S b
>>= a -> S b
k = forall a. (RW -> Answer (a, RW)) -> S a
S 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 :: forall a. S a
empty = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  <|> :: forall a. S a -> S a -> S a
(<|>) = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus

instance MonadPlus S where
  mzero :: forall a. S a
mzero = forall a. (RW -> Answer (a, RW)) -> S a
S forall a b. (a -> b) -> a -> b
$ \RW
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
  mplus :: forall a. S a -> S a -> S a
mplus (S RW -> Answer (a, RW)
m1) (S RW -> Answer (a, RW)
m2) = forall a. (RW -> Answer (a, RW)) -> S a
S forall a b. (a -> b) -> a -> b
$ \RW
s -> 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 :: forall a b. (a -> b) -> S a -> S b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative S where
  pure :: forall a. a -> S a
pure a
a = forall a. (RW -> Answer (a, RW)) -> S a
S forall a b. (a -> b) -> a -> b
$ \RW
s -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, RW
s)
  <*> :: forall a 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 :: forall a. (RW -> (a, RW)) -> S a
updS RW -> (a, RW)
f = forall a. (RW -> Answer (a, RW)) -> S a
S forall a b. (a -> b) -> a -> b
$ \RW
s -> 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 = forall a. (RW -> (a, RW)) -> S a
updS forall a b. (a -> b) -> a -> b
$ \RW
rw -> ((), RW -> RW
f RW
rw)

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

newVar :: S Name
newVar :: S Name
newVar = forall a. (RW -> (a, RW)) -> S a
updS 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 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 = forall a. (RW -> a) -> S a
get forall a b. (a -> b) -> a -> b
$ \RW
rw -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap ([Bound], [Bound])
bounds 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 -> forall a b. (a, b) -> a
fst ([Bound], [Bound])
bs
    BoundType
Upper -> 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_ 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 forall a. [a] -> [a] -> [a]
++ [a]
oldL, [a]
newU forall a. [a] -> [a] -> [a]
++ [a]
oldU)
   in RW
rw {inerts :: Inerts
inerts = Inerts
i {bounds :: NameMap ([Bound], [Bound])
bounds = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith 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 <- forall a. (RW -> (a, RW)) -> S a
updS 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})
    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 <- forall a. (RW -> a) -> S a
get RW -> Inerts
inerts
    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]
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
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
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
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
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) = forall a. a -> Maybe a
Just Int
x
fromName (SysName 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
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
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
Ord)

infixl 6 |+|, |-|

infixr 7 |*|

-- | A constant term.
tConst :: Integer -> Term
tConst :: Integer -> Term
tConst Integer
k = Integer -> NameMap Integer -> Term
T Integer
k 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 (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 forall a. Num a => a -> a -> a
+ Integer
n2) forall a b. (a -> b) -> a -> b
$
    if forall k a. Map k a -> Bool
Map.null NameMap Integer
m1
      then NameMap Integer
m2
      else
        if forall k a. Map k a -> Bool
Map.null NameMap Integer
m2
          then NameMap Integer
m1
          else forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall a. Eq a => a -> a -> Bool
/= Integer
0) forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith 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 forall a. Num a => a -> a -> a
* Integer
n) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer
k 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 forall a. Num a => a -> a -> a
* Integer
k 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 = 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 = forall a. Show a => Int -> a -> ShowS
showsPrec Int
c (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 forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
m of
    [] -> Integer -> Doc
integer Integer
k
    [(Name, Integer)]
xs | Integer
k forall a. Eq a => a -> a -> Bool
/= Integer
0 -> [Doc] -> Doc
hsep (Integer -> Doc
integer Integer
k forall a. a -> [a] -> [a]
: 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 forall a. a -> [a] -> [a]
: 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 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 (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 forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\Name
_ 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) = 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)
  | forall k a. Map k a -> Bool
Map.null NameMap Integer
m = forall a. a -> Maybe a
Just Integer
n
  | Bool
otherwise = 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 forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
m of
  [(Name
x, Integer
b)] -> forall a. a -> Maybe a
Just (Integer
a, Integer
b, Name
x)
  [(Name, Integer)]
_ -> 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) = forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition (\Integer
x -> Integer
x forall a. Eq a => a -> a -> Bool
== Integer
1 Bool -> Bool -> Bool
|| Integer
x forall a. Eq a => a -> a -> Bool
== -Integer
1) NameMap Integer
m
    ((Name
x, Integer
xc), NameMap Integer
m3) <- forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey NameMap Integer
m1
    forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
xc, Name
x, Integer -> NameMap Integer -> Term
T Integer
a (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) = 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 forall a. a -> [a] -> [a]
: forall k a. Map k a -> [a]
Map.elems NameMap Integer
m)
    forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
d, Integer -> NameMap Integer -> Term
T (forall a. Integral a => a -> a -> a
div Integer
c Integer
d) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Integral a => a -> a -> a
`div` Integer
d) NameMap Integer
m))
  where
    common :: [Integer] -> Maybe Integer
    common :: [Integer] -> Maybe Integer
common [] = forall a. Maybe a
Nothing
    common [Integer
x] = forall a. a -> Maybe a
Just Integer
x
    common (Integer
x : Integer
y : [Integer]
zs) =
      case forall a. Integral a => a -> a -> a
gcd Integer
x Integer
y of
        Integer
1 -> forall a. Maybe a
Nothing
        Integer
n -> [Integer] -> Maybe Integer
common (Integer
n 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) <- forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey forall {a}.
(Ord a, Num a) =>
Name
-> a
-> Maybe (a, Name, NameMap Integer)
-> Maybe (a, Name, NameMap Integer)
step forall a. Maybe a
Nothing NameMap Integer
m
  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 = forall a. a -> Maybe a
Just (a
xc, Name
x, 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
_))
      | forall a. Num a => a -> a
abs a
xc forall a. Ord a => a -> a -> Bool
< forall a. Num a => a -> a
abs a
yc = forall a. a -> Maybe a
Just (a
xc, Name
x, 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) <- forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey NameMap Integer
m
    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) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f NameMap Integer
m)