{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Safe #-}
module Data.Integer.SAT (
PropSet,
noProps,
checkSat,
assert,
Prop (..),
Expr (..),
BoundType (..),
getExprBound,
getExprRange,
Name,
toName,
fromName,
allSolutions,
slnCurrent,
slnNextVal,
slnNextVar,
slnEnumerate,
dotPropSet,
sizePropSet,
allInerts,
ppInerts,
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 :*
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
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
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
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
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)
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]]
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)
data Expr
=
Expr :+ Expr
|
Expr :- Expr
|
Integer :* Expr
|
Negate Expr
|
Var Name
|
K Integer
|
If Prop Expr Expr
|
Div Expr Integer
|
Mod Expr Integer
|
Min Expr Expr
|
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)
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}
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
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
data Inerts = Inerts
{ Inerts -> NameMap ([Bound], [Bound])
bounds :: NameMap ([Bound], [Bound])
, Inerts -> NameMap Term
solved :: NameMap Term
}
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
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
}
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
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) =
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)
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)
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
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
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
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)
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)
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
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
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
solveIs0' :: Term -> S ()
solveIs0' :: Term -> S ()
solveIs0' Term
t
| 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)
| 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
| 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)
| Just (Integer
_, Term
s) <- Term -> Maybe (Integer, Term)
tFactor Term
t = Term -> S ()
solveIs0 Term
s
| 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
solveIsNeg' :: Term -> S ()
solveIsNeg' :: Term -> S ()
solveIsNeg' Term
t
| 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)
| Just (Integer
_, Term
s) <- Term -> Maybe (Integer, Term)
tFactor Term
t = Term -> S ()
solveIsNeg Term
s
| 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
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
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]
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
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 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}
)
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)}}
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
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 |*|
tConst :: Integer -> Term
tConst :: Integer -> Term
tConst Integer
k = Integer -> NameMap Integer -> Term
T Integer
k forall k a. Map k a
Map.empty
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
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
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
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
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)
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
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
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
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
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)
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
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)
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)