{-# LANGUAGE BangPatterns, CPP, PatternGuards, 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 Prelude hiding ((<>))
import Text.PrettyPrint
infixr 2 :||
infixr 3 :&&
infix 4 :==, :/=, :<, :<=, :>, :>=
infixl 6 :+, :-
infixl 7 :*
newtype PropSet = State (Answer RW)
deriving Int -> PropSet -> ShowS
[PropSet] -> ShowS
PropSet -> String
(Int -> PropSet -> ShowS)
-> (PropSet -> String) -> ([PropSet] -> ShowS) -> Show PropSet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropSet] -> ShowS
$cshowList :: [PropSet] -> ShowS
show :: PropSet -> String
$cshow :: PropSet -> String
showsPrec :: Int -> PropSet -> ShowS
$cshowsPrec :: Int -> PropSet -> ShowS
Show
dotPropSet :: PropSet -> Doc
dotPropSet :: PropSet -> Doc
dotPropSet (State Answer RW
a) = (RW -> Doc) -> Answer RW -> Doc
forall a. (a -> Doc) -> Answer a -> Doc
dotAnswer (Inerts -> Doc
ppInerts (Inerts -> Doc) -> (RW -> Inerts) -> RW -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> Inerts
inerts) Answer RW
a
sizePropSet :: PropSet -> (Integer,Integer,Integer)
sizePropSet :: PropSet -> (Integer, Integer, Integer)
sizePropSet (State Answer RW
a) = Answer RW -> (Integer, Integer, Integer)
forall a. Answer a -> (Integer, Integer, Integer)
answerSize Answer RW
a
noProps :: PropSet
noProps :: PropSet
noProps = Answer RW -> PropSet
State (Answer RW -> PropSet) -> Answer RW -> PropSet
forall a b. (a -> b) -> a -> b
$ RW -> Answer RW
forall (m :: * -> *) a. Monad m => a -> m a
return RW
initRW
assert :: Prop -> PropSet -> PropSet
assert :: Prop -> PropSet -> PropSet
assert Prop
p (State Answer RW
rws) = Answer RW -> PropSet
State (Answer RW -> PropSet) -> Answer RW -> PropSet
forall a b. (a -> b) -> a -> b
$ (((), RW) -> RW) -> Answer ((), RW) -> Answer RW
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), RW) -> RW
forall a b. (a, b) -> b
snd (Answer ((), RW) -> Answer RW) -> Answer ((), RW) -> Answer RW
forall a b. (a -> b) -> a -> b
$ RW -> Answer ((), RW)
m (RW -> Answer ((), RW)) -> Answer RW -> Answer ((), RW)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Answer RW
rws
where S RW -> Answer ((), RW)
m = Prop -> S ()
prop Prop
p
checkSat :: PropSet -> Maybe [(Int,Integer)]
checkSat :: PropSet -> Maybe [(Int, Integer)]
checkSat (State Answer RW
m) = Answer RW -> Maybe [(Int, Integer)]
forall (m :: * -> *).
MonadPlus m =>
Answer RW -> m [(Int, Integer)]
go Answer RW
m
where
go :: Answer RW -> m [(Int, Integer)]
go Answer RW
None = m [(Int, Integer)]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
go (One RW
rw) = [(Int, Integer)] -> m [(Int, Integer)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Int
x,Integer
v) | (UserName Int
x, Integer
v) <- Inerts -> [(Name, Integer)]
iModel (RW -> Inerts
inerts RW
rw) ]
go (Choice Answer RW
m1 Answer RW
m2) = m [(Int, Integer)] -> m [(Int, Integer)] -> m [(Int, Integer)]
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (Answer RW -> m [(Int, Integer)]
go Answer RW
m1) (Answer RW -> m [(Int, Integer)]
go Answer RW
m2)
allInerts :: PropSet -> [Inerts]
allInerts :: PropSet -> [Inerts]
allInerts (State Answer RW
m) = (RW -> Inerts) -> [RW] -> [Inerts]
forall a b. (a -> b) -> [a] -> [b]
map RW -> Inerts
inerts (Answer RW -> [RW]
forall a. Answer a -> [a]
toList Answer RW
m)
allSolutions :: PropSet -> [Solutions]
allSolutions :: PropSet -> [Solutions]
allSolutions = (Inerts -> Solutions) -> [Inerts] -> [Solutions]
forall a b. (a -> b) -> [a] -> [b]
map Inerts -> Solutions
startIter ([Inerts] -> [Solutions])
-> (PropSet -> [Inerts]) -> PropSet -> [Solutions]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropSet -> [Inerts]
allInerts
getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer
getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer
getExprBound BoundType
bt Expr
e (State Answer RW
s) =
do let S RW -> Answer (Term, RW)
m = Expr -> S Term
expr Expr
e
check :: (Term, RW) -> Maybe Integer
check (Term
t,RW
s1) = BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt Term
t (RW -> Inerts
inerts RW
s1)
[Integer]
bs <- ((Term, RW) -> Maybe Integer) -> [(Term, RW)] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, RW) -> Maybe Integer
check ([(Term, RW)] -> Maybe [Integer])
-> [(Term, RW)] -> Maybe [Integer]
forall a b. (a -> b) -> a -> b
$ Answer (Term, RW) -> [(Term, RW)]
forall a. Answer a -> [a]
toList (Answer (Term, RW) -> [(Term, RW)])
-> Answer (Term, RW) -> [(Term, RW)]
forall a b. (a -> b) -> a -> b
$ Answer RW
s Answer RW -> (RW -> Answer (Term, RW)) -> Answer (Term, RW)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RW -> Answer (Term, RW)
m
case [Integer]
bs of
[] -> Maybe Integer
forall a. Maybe a
Nothing
[Integer]
_ -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
bs)
getExprRange :: Expr -> PropSet -> Maybe [Integer]
getExprRange :: Expr -> PropSet -> Maybe [Integer]
getExprRange Expr
e (State Answer RW
s) =
do let S RW -> Answer (Term, RW)
m = Expr -> S Term
expr Expr
e
check :: (Term, RW) -> Maybe (Integer, Integer)
check (Term
t,RW
s1) = do Integer
l <- BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
Lower Term
t (RW -> Inerts
inerts RW
s1)
Integer
u <- BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
Upper Term
t (RW -> Inerts
inerts RW
s1)
(Integer, Integer) -> Maybe (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
l,Integer
u)
[(Integer, Integer)]
bs <- ((Term, RW) -> Maybe (Integer, Integer))
-> [(Term, RW)] -> Maybe [(Integer, Integer)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term, RW) -> Maybe (Integer, Integer)
check ([(Term, RW)] -> Maybe [(Integer, Integer)])
-> [(Term, RW)] -> Maybe [(Integer, Integer)]
forall a b. (a -> b) -> a -> b
$ Answer (Term, RW) -> [(Term, RW)]
forall a. Answer a -> [a]
toList (Answer (Term, RW) -> [(Term, RW)])
-> Answer (Term, RW) -> [(Term, RW)]
forall a b. (a -> b) -> a -> b
$ Answer RW
s Answer RW -> (RW -> Answer (Term, RW)) -> Answer (Term, RW)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RW -> Answer (Term, RW)
m
case [(Integer, Integer)]
bs of
[] -> Maybe [Integer]
forall a. Maybe a
Nothing
[(Integer, Integer)]
_ -> let ([Integer]
ls,[Integer]
us) = [(Integer, Integer)] -> ([Integer], [Integer])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Integer, Integer)]
bs
in [Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just [ Integer
x | Integer
x <- [ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
ls .. [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
us ] ]
data Prop = PTrue
| PFalse
| Prop :|| Prop
| Prop :&& Prop
| Not Prop
| Expr :== Expr
| Expr :/= Expr
| Expr :< Expr
| Expr :> Expr
| Expr :<= Expr
| Expr :>= Expr
deriving (ReadPrec [Prop]
ReadPrec Prop
Int -> ReadS Prop
ReadS [Prop]
(Int -> ReadS Prop)
-> ReadS [Prop] -> ReadPrec Prop -> ReadPrec [Prop] -> Read Prop
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Prop]
$creadListPrec :: ReadPrec [Prop]
readPrec :: ReadPrec Prop
$creadPrec :: ReadPrec Prop
readList :: ReadS [Prop]
$creadList :: ReadS [Prop]
readsPrec :: Int -> ReadS Prop
$creadsPrec :: Int -> ReadS Prop
Read,Int -> Prop -> ShowS
[Prop] -> ShowS
Prop -> String
(Int -> Prop -> ShowS)
-> (Prop -> String) -> ([Prop] -> ShowS) -> Show Prop
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prop] -> ShowS
$cshowList :: [Prop] -> ShowS
show :: Prop -> String
$cshow :: Prop -> String
showsPrec :: Int -> Prop -> ShowS
$cshowsPrec :: Int -> Prop -> ShowS
Show,Eq Prop
Eq Prop
-> (Prop -> Prop -> Ordering)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Bool)
-> (Prop -> Prop -> Prop)
-> (Prop -> Prop -> Prop)
-> Ord Prop
Prop -> Prop -> Bool
Prop -> Prop -> Ordering
Prop -> Prop -> Prop
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Prop -> Prop -> Prop
$cmin :: Prop -> Prop -> Prop
max :: Prop -> Prop -> Prop
$cmax :: Prop -> Prop -> Prop
>= :: Prop -> Prop -> Bool
$c>= :: Prop -> Prop -> Bool
> :: Prop -> Prop -> Bool
$c> :: Prop -> Prop -> Bool
<= :: Prop -> Prop -> Bool
$c<= :: Prop -> Prop -> Bool
< :: Prop -> Prop -> Bool
$c< :: Prop -> Prop -> Bool
compare :: Prop -> Prop -> Ordering
$ccompare :: Prop -> Prop -> Ordering
$cp1Ord :: Eq Prop
Ord, Prop -> Prop -> Bool
(Prop -> Prop -> Bool) -> (Prop -> Prop -> Bool) -> Eq Prop
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prop -> Prop -> Bool
$c/= :: Prop -> Prop -> Bool
== :: Prop -> Prop -> Bool
$c== :: Prop -> Prop -> Bool
Eq)
data Expr = Expr :+ Expr
| Expr :- Expr
| Integer :* Expr
| Negate Expr
| Var Name
| K Integer
| If Prop Expr Expr
| Div Expr Integer
| Mod Expr Integer
deriving (ReadPrec [Expr]
ReadPrec Expr
Int -> ReadS Expr
ReadS [Expr]
(Int -> ReadS Expr)
-> ReadS [Expr] -> ReadPrec Expr -> ReadPrec [Expr] -> Read Expr
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Expr]
$creadListPrec :: ReadPrec [Expr]
readPrec :: ReadPrec Expr
$creadPrec :: ReadPrec Expr
readList :: ReadS [Expr]
$creadList :: ReadS [Expr]
readsPrec :: Int -> ReadS Expr
$creadsPrec :: Int -> ReadS Expr
Read,Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, Eq Expr
Eq Expr
-> (Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Expr)
-> (Expr -> Expr -> Expr)
-> Ord Expr
Expr -> Expr -> Bool
Expr -> Expr -> Ordering
Expr -> Expr -> Expr
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$c>= :: Expr -> Expr -> Bool
> :: Expr -> Expr -> Bool
$c> :: Expr -> Expr -> Bool
<= :: Expr -> Expr -> Bool
$c<= :: Expr -> Expr -> Bool
< :: Expr -> Expr -> Bool
$c< :: Expr -> Expr -> Bool
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
$cp1Ord :: Eq Expr
Ord, Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq)
prop :: Prop -> S ()
prop :: Prop -> S ()
prop Prop
PTrue = () -> S ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
prop Prop
PFalse = S ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
prop (Prop
p1 :|| Prop
p2) = Prop -> S ()
prop Prop
p1 S () -> S () -> S ()
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Prop -> S ()
prop Prop
p2
prop (Prop
p1 :&& Prop
p2) = Prop -> S ()
prop Prop
p1 S () -> S () -> S ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Prop -> S ()
prop Prop
p2
prop (Not Prop
p) = Prop -> S ()
prop (Prop -> Prop
neg Prop
p)
where
neg :: Prop -> Prop
neg Prop
PTrue = Prop
PFalse
neg Prop
PFalse = Prop
PTrue
neg (Prop
p1 :&& Prop
p2) = Prop -> Prop
neg Prop
p1 Prop -> Prop -> Prop
:|| Prop -> Prop
neg Prop
p2
neg (Prop
p1 :|| Prop
p2) = Prop -> Prop
neg Prop
p1 Prop -> Prop -> Prop
:&& Prop -> Prop
neg Prop
p2
neg (Not Prop
q) = Prop
q
neg (Expr
e1 :== Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:/= Expr
e2
neg (Expr
e1 :/= Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:== Expr
e2
neg (Expr
e1 :< Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:>= Expr
e2
neg (Expr
e1 :<= Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:> Expr
e2
neg (Expr
e1 :> Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:<= Expr
e2
neg (Expr
e1 :>= Expr
e2) = Expr
e1 Expr -> Expr -> Prop
:< Expr
e2
prop (Expr
e1 :== Expr
e2) = do Term
t1 <- Expr -> S Term
expr Expr
e1
Term
t2 <- Expr -> S Term
expr Expr
e2
Term -> S ()
solveIs0 (Term
t1 Term -> Term -> Term
|-| Term
t2)
prop (Expr
e1 :/= Expr
e2) = do Term
t1 <- Expr -> S Term
expr Expr
e1
Term
t2 <- Expr -> S Term
expr Expr
e2
let t :: Term
t = Term
t1 Term -> Term -> Term
|-| Term
t2
Term -> S ()
solveIsNeg Term
t S () -> S () -> S ()
`orElse` Term -> S ()
solveIsNeg (Term -> Term
tNeg Term
t)
prop (Expr
e1 :< Expr
e2) = do Term
t1 <- Expr -> S Term
expr Expr
e1
Term
t2 <- Expr -> S Term
expr Expr
e2
Term -> S ()
solveIsNeg (Term
t1 Term -> Term -> Term
|-| Term
t2)
prop (Expr
e1 :<= Expr
e2) = do Term
t1 <- Expr -> S Term
expr Expr
e1
Term
t2 <- Expr -> S Term
expr Expr
e2
let t :: Term
t = Term
t1 Term -> Term -> Term
|-| Term
t2 Term -> Term -> Term
|-| Integer -> Term
tConst Integer
1
Term -> S ()
solveIsNeg Term
t
prop (Expr
e1 :> Expr
e2) = Prop -> S ()
prop (Expr
e2 Expr -> Expr -> Prop
:< Expr
e1)
prop (Expr
e1 :>= Expr
e2) = Prop -> S ()
prop (Expr
e2 Expr -> Expr -> Prop
:<= Expr
e1)
expr :: Expr -> S Term
expr :: Expr -> S Term
expr (Expr
e1 :+ Expr
e2) = Term -> Term -> Term
(|+|) (Term -> Term -> Term) -> S Term -> S (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e1 S (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> S Term
expr Expr
e2
expr (Expr
e1 :- Expr
e2) = Term -> Term -> Term
(|-|) (Term -> Term -> Term) -> S Term -> S (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e1 S (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> S Term
expr Expr
e2
expr (Integer
k :* Expr
e2) = (Integer
k Integer -> Term -> Term
|*|) (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e2
expr (Negate Expr
e) = Term -> Term
tNeg (Term -> Term) -> S Term -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> S Term
expr Expr
e
expr (Var Name
x) = Term -> S Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Term
tVar Name
x)
expr (K Integer
x) = Term -> S Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Term
tConst Integer
x)
expr (If Prop
p Expr
e1 Expr
e2) = do Name
x <- S Name
newVar
Prop -> S ()
prop (Prop
p Prop -> Prop -> Prop
:&& Name -> Expr
Var Name
x Expr -> Expr -> Prop
:== Expr
e1 Prop -> Prop -> Prop
:|| Prop -> Prop
Not Prop
p Prop -> Prop -> Prop
:&& Name -> Expr
Var Name
x Expr -> Expr -> Prop
:== Expr
e2)
Term -> S Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Term
tVar Name
x)
expr (Div Expr
e Integer
k) = ((Term, Term) -> Term) -> S (Term, Term) -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> a
fst (S (Term, Term) -> S Term) -> S (Term, Term) -> S Term
forall a b. (a -> b) -> a -> b
$ Expr -> Integer -> S (Term, Term)
exprDivMod Expr
e Integer
k
expr (Mod Expr
e Integer
k) = ((Term, Term) -> Term) -> S (Term, Term) -> S Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> b
snd (S (Term, Term) -> S Term) -> S (Term, Term) -> S Term
forall a b. (a -> b) -> a -> b
$ Expr -> Integer -> S (Term, Term)
exprDivMod Expr
e Integer
k
exprDivMod :: Expr -> Integer -> S (Term,Term)
exprDivMod :: Expr -> Integer -> S (Term, Term)
exprDivMod Expr
e Integer
k =
do Bool -> S ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0)
Name
q <- S Name
newVar
Name
r <- S Name
newVar
let er :: Expr
er = Name -> Expr
Var Name
r
Prop -> S ()
prop (Integer
k Integer -> Expr -> Expr
:* Name -> Expr
Var Name
q Expr -> Expr -> Expr
:+ Expr
er Expr -> Expr -> Prop
:== Expr
e Prop -> Prop -> Prop
:&& Expr
er Expr -> Expr -> Prop
:< Integer -> Expr
K Integer
k Prop -> Prop -> Prop
:&& Integer -> Expr
K Integer
0 Expr -> Expr -> Prop
:<= Expr
er)
(Term, Term) -> S (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Term
tVar Name
q, Name -> Term
tVar Name
r)
data RW = RW { RW -> Int
nameSource :: !Int
, RW -> Inerts
inerts :: Inerts
} deriving Int -> RW -> ShowS
[RW] -> ShowS
RW -> String
(Int -> RW -> ShowS)
-> (RW -> String) -> ([RW] -> ShowS) -> Show RW
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RW] -> ShowS
$cshowList :: [RW] -> ShowS
show :: RW -> String
$cshow :: RW -> String
showsPrec :: Int -> RW -> ShowS
$cshowsPrec :: Int -> RW -> ShowS
Show
initRW :: RW
initRW :: RW
initRW = RW :: Int -> Inerts -> RW
RW { nameSource :: Int
nameSource = Int
0, inerts :: Inerts
inerts = Inerts
iNone }
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
(Int -> Bound -> ShowS)
-> (Bound -> String) -> ([Bound] -> ShowS) -> Show Bound
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Bound] -> ShowS
$cshowList :: [Bound] -> ShowS
show :: Bound -> String
$cshow :: Bound -> String
showsPrec :: Int -> Bound -> ShowS
$cshowsPrec :: Int -> Bound -> ShowS
Show
data BoundType = Lower | Upper
deriving Int -> BoundType -> ShowS
[BoundType] -> ShowS
BoundType -> String
(Int -> BoundType -> ShowS)
-> (BoundType -> String)
-> ([BoundType] -> ShowS)
-> Show BoundType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BoundType] -> ShowS
$cshowList :: [BoundType] -> ShowS
show :: BoundType -> String
$cshow :: BoundType -> String
showsPrec :: Int -> BoundType -> ShowS
$cshowsPrec :: Int -> BoundType -> ShowS
Show
toCt :: BoundType -> Name -> Bound -> Term
toCt :: BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
x (Bound Integer
c Term
t) = Term -> Term -> Term
ctLt Term
t (Integer
c Integer -> Term -> Term
|*| Name -> Term
tVar Name
x)
toCt BoundType
Upper Name
x (Bound Integer
c Term
t) = Term -> Term -> Term
ctLt (Integer
c Integer -> Term -> Term
|*| Name -> Term
tVar Name
x) Term
t
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
(Int -> Inerts -> ShowS)
-> (Inerts -> String) -> ([Inerts] -> ShowS) -> Show Inerts
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Inerts] -> ShowS
$cshowList :: [Inerts] -> ShowS
show :: Inerts -> String
$cshow :: Inerts -> String
showsPrec :: Int -> Inerts -> ShowS
$cshowsPrec :: Int -> Inerts -> ShowS
Show
ppInerts :: Inerts -> Doc
ppInerts :: Inerts -> Doc
ppInerts Inerts
is = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [ Name -> Bound -> Doc
ppLower Name
x Bound
b | (Name
x,([Bound]
ls,[Bound]
_)) <- [(Name, ([Bound], [Bound]))]
bnds, Bound
b <- [Bound]
ls ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
[ Name -> Bound -> Doc
ppUpper Name
x Bound
b | (Name
x,([Bound]
_,[Bound]
us)) <- [(Name, ([Bound], [Bound]))]
bnds, Bound
b <- [Bound]
us ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
[ (Name, Term) -> Doc
ppEq (Name, Term)
e | (Name, Term)
e <- NameMap Term -> [(Name, Term)]
forall k a. Map k a -> [(k, a)]
Map.toList (Inerts -> NameMap Term
solved Inerts
is) ]
where
bnds :: [(Name, ([Bound], [Bound]))]
bnds = NameMap ([Bound], [Bound]) -> [(Name, ([Bound], [Bound]))]
forall k a. Map k a -> [(k, a)]
Map.toList (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is)
ppT :: Integer -> Name -> Doc
ppT Integer
c Name
x = Term -> Doc
ppTerm (Integer
c Integer -> Term -> Term
|*| Name -> Term
tVar Name
x)
ppLower :: Name -> Bound -> Doc
ppLower Name
x (Bound Integer
c Term
t) = Term -> Doc
ppTerm Term
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"<" Doc -> Doc -> Doc
<+> Integer -> Name -> Doc
ppT Integer
c Name
x
ppUpper :: Name -> Bound -> Doc
ppUpper Name
x (Bound Integer
c Term
t) = Integer -> Name -> Doc
ppT Integer
c Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"<" Doc -> Doc -> Doc
<+> Term -> Doc
ppTerm Term
t
ppEq :: (Name, Term) -> Doc
ppEq (Name
x,Term
t) = Name -> Doc
ppName Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> Term -> Doc
ppTerm Term
t
iNone :: Inerts
iNone :: Inerts
iNone = Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
Inerts { bounds :: NameMap ([Bound], [Bound])
bounds = NameMap ([Bound], [Bound])
forall k a. Map k a
Map.empty
, solved :: NameMap Term
solved = NameMap Term
forall k a. Map k a
Map.empty
}
iApSubst :: Inerts -> Term -> Term
iApSubst :: Inerts -> Term -> Term
iApSubst Inerts
i Term
t = ((Name, Term) -> Term -> Term) -> Term -> [(Name, Term)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Name, Term) -> Term -> Term
apS Term
t ([(Name, Term)] -> Term) -> [(Name, Term)] -> Term
forall a b. (a -> b) -> a -> b
$ NameMap Term -> [(Name, Term)]
forall k a. Map k a -> [(k, a)]
Map.toList (NameMap Term -> [(Name, Term)]) -> NameMap Term -> [(Name, Term)]
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap Term
solved Inerts
i
where apS :: (Name, Term) -> Term -> Term
apS (Name
x,Term
t1) Term
t2 = Name -> Term -> Term -> Term
tLet Name
x Term
t1 Term
t2
iSolved :: Name -> Term -> Inerts -> ([Term], Inerts)
iSolved :: Name -> Term -> Inerts -> ([Term], Inerts)
iSolved Name
x Term
t Inerts
i =
( [Term]
kickedOut
, Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
Inerts { bounds :: NameMap ([Bound], [Bound])
bounds = NameMap ([Bound], [Bound])
otherBounds
, solved :: NameMap Term
solved = Name -> Term -> NameMap Term -> NameMap Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Term
t (NameMap Term -> NameMap Term) -> NameMap Term -> NameMap Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> NameMap Term -> NameMap Term
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Name -> Term -> Term -> Term
tLet Name
x Term
t) (NameMap Term -> NameMap Term) -> NameMap Term -> NameMap Term
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap Term
solved Inerts
i
}
)
where
([Term]
kickedOut, NameMap ([Bound], [Bound])
otherBounds) =
let (Maybe ([Bound], [Bound])
mb, NameMap ([Bound], [Bound])
mp1) = (Name -> ([Bound], [Bound]) -> Maybe ([Bound], [Bound]))
-> Name
-> NameMap ([Bound], [Bound])
-> (Maybe ([Bound], [Bound]), NameMap ([Bound], [Bound]))
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\Name
_ ([Bound], [Bound])
_ -> Maybe ([Bound], [Bound])
forall a. Maybe a
Nothing) Name
x (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
i)
mp2 :: Map Name (([Bound], [Bound]), [Term])
mp2 = (Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term]))
-> NameMap ([Bound], [Bound])
-> Map Name (([Bound], [Bound]), [Term])
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term])
extractBounds NameMap ([Bound], [Bound])
mp1
in ( [ Term
ct | ([Bound]
lbs,[Bound]
ubs) <- Maybe ([Bound], [Bound]) -> [([Bound], [Bound])]
forall a. Maybe a -> [a]
maybeToList Maybe ([Bound], [Bound])
mb
, Term
ct <- (Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
x) [Bound]
lbs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ (Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Upper Name
x) [Bound]
ubs ]
[Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++
[ Term
ct | (([Bound], [Bound])
_,[Term]
cts) <- Map Name (([Bound], [Bound]), [Term])
-> [(([Bound], [Bound]), [Term])]
forall k a. Map k a -> [a]
Map.elems Map Name (([Bound], [Bound]), [Term])
mp2, Term
ct <- [Term]
cts ]
, ((([Bound], [Bound]), [Term]) -> ([Bound], [Bound]))
-> Map Name (([Bound], [Bound]), [Term])
-> NameMap ([Bound], [Bound])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Bound], [Bound]), [Term]) -> ([Bound], [Bound])
forall a b. (a, b) -> a
fst Map Name (([Bound], [Bound]), [Term])
mp2
)
extractBounds :: Name -> ([Bound], [Bound]) -> (([Bound], [Bound]), [Term])
extractBounds Name
y ([Bound]
lbs,[Bound]
ubs) =
let ([Bound]
lbsStay, [Bound]
lbsKick) = (Bound -> Bool) -> [Bound] -> ([Bound], [Bound])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Bound -> Bool
stay [Bound]
lbs
([Bound]
ubsStay, [Bound]
ubsKick) = (Bound -> Bool) -> [Bound] -> ([Bound], [Bound])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Bound -> Bool
stay [Bound]
ubs
in ( ([Bound]
lbsStay,[Bound]
ubsStay)
, (Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Lower Name
y) [Bound]
lbsKick [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++
(Bound -> Term) -> [Bound] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (BoundType -> Name -> Bound -> Term
toCt BoundType
Upper Name
y) [Bound]
ubsKick
)
stay :: Bound -> Bool
stay (Bound Integer
_ Term
bnd) = Bool -> Bool
not (Name -> Term -> Bool
tHasVar Name
x Term
bnd)
boundInterval :: [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
boundInterval :: [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
boundInterval [Bound]
lbs [Bound]
ubs =
do [Integer]
ls <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BoundType -> Bound -> Maybe Integer
normBound BoundType
Lower) [Bound]
lbs
[Integer]
us <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BoundType -> Bound -> Maybe Integer
normBound BoundType
Upper) [Bound]
ubs
let lb :: Maybe Integer
lb = case [Integer]
ls of
[] -> Maybe Integer
forall a. Maybe a
Nothing
[Integer]
_ -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
ls Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
ub :: Maybe Integer
ub = case [Integer]
us of
[] -> Maybe Integer
forall a. Maybe a
Nothing
[Integer]
_ -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
us Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
case (Maybe Integer
lb,Maybe Integer
ub) of
(Just Integer
l, Just Integer
u) -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
u)
(Maybe Integer, Maybe Integer)
_ -> () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Maybe Integer, Maybe Integer)
-> Maybe (Maybe Integer, Maybe Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
lb,Maybe Integer
ub)
where
normBound :: BoundType -> Bound -> Maybe Integer
normBound BoundType
Lower (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer
c)
normBound BoundType
Upper (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
k Integer
c)
data Solutions = Done
| TopVar Name Integer (Maybe Integer) (Maybe Integer) Inerts
| FixedVar Name Integer Solutions
deriving Int -> Solutions -> ShowS
[Solutions] -> ShowS
Solutions -> String
(Int -> Solutions -> ShowS)
-> (Solutions -> String)
-> ([Solutions] -> ShowS)
-> Show Solutions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Solutions] -> ShowS
$cshowList :: [Solutions] -> ShowS
show :: Solutions -> String
$cshow :: Solutions -> String
showsPrec :: Int -> Solutions -> ShowS
$cshowsPrec :: Int -> Solutions -> ShowS
Show
slnCurrent :: Solutions -> [(Int,Integer)]
slnCurrent :: Solutions -> [(Int, Integer)]
slnCurrent Solutions
s = [ (Int
x,Integer
v) | (UserName Int
x, Integer
v) <- Solutions -> [(Name, Integer)]
go Solutions
s ]
where
go :: Solutions -> [(Name, Integer)]
go Solutions
Done = []
go (TopVar Name
x Integer
v Maybe Integer
_ Maybe Integer
_ Inerts
is) = (Name
x, Integer
v) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: Inerts -> [(Name, Integer)]
iModel (Name -> Integer -> Inerts -> Inerts
iLet Name
x Integer
v Inerts
is)
go (FixedVar Name
x Integer
v Solutions
i) = (Name
x, Integer
v) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: Solutions -> [(Name, Integer)]
go Solutions
i
iLet :: Name -> Integer -> Inerts -> Inerts
iLet :: Name -> Integer -> Inerts -> Inerts
iLet Name
x Integer
v Inerts
is = Inerts :: NameMap ([Bound], [Bound]) -> NameMap Term -> Inerts
Inerts { bounds :: NameMap ([Bound], [Bound])
bounds = (([Bound], [Bound]) -> ([Bound], [Bound]))
-> NameMap ([Bound], [Bound]) -> NameMap ([Bound], [Bound])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Bound], [Bound]) -> ([Bound], [Bound])
updBs (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is)
, solved :: NameMap Term
solved = (Term -> Term) -> NameMap Term -> NameMap Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Integer -> Term -> Term
tLetNum Name
x Integer
v) (Inerts -> NameMap Term
solved Inerts
is) }
where
updB :: Bound -> Bound
updB (Bound Integer
c Term
t) = Integer -> Term -> Bound
Bound Integer
c (Name -> Integer -> Term -> Term
tLetNum Name
x Integer
v Term
t)
updBs :: ([Bound], [Bound]) -> ([Bound], [Bound])
updBs ([Bound]
ls,[Bound]
us) = ((Bound -> Bound) -> [Bound] -> [Bound]
forall a b. (a -> b) -> [a] -> [b]
map Bound -> Bound
updB [Bound]
ls, (Bound -> Bound) -> [Bound] -> [Bound]
forall a b. (a -> b) -> [a] -> [b]
map Bound -> Bound
updB [Bound]
us)
startIter :: Inerts -> Solutions
startIter :: Inerts -> Solutions
startIter Inerts
is =
case NameMap ([Bound], [Bound])
-> Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is) of
Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
Nothing ->
case NameMap Term -> Maybe ((Name, Term), NameMap Term)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey (Inerts -> NameMap Term
solved Inerts
is) of
Maybe ((Name, Term), NameMap Term)
Nothing -> Solutions
Done
Just ((Name
x,Term
t), NameMap Term
mp1) ->
case [ Name
y | Name
y <- Term -> [Name]
tVarList Term
t ] of
Name
y : [Name]
_ -> Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
y Integer
0 Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing Inerts
is
[] -> let v :: Integer
v = Term -> Integer
tConstPart Term
t
in Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
x Integer
v (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
v) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
v) (Inerts -> Solutions) -> Inerts -> Solutions
forall a b. (a -> b) -> a -> b
$ Inerts
is { solved :: NameMap Term
solved = NameMap Term
mp1 }
Just ((Name
x,([Bound]
lbs,[Bound]
ubs)), NameMap ([Bound], [Bound])
mp1) ->
case [ Name
y | Bound Integer
_ Term
t <- [Bound]
lbs [Bound] -> [Bound] -> [Bound]
forall a. [a] -> [a] -> [a]
++ [Bound]
ubs, Name
y <- Term -> [Name]
tVarList Term
t ] of
Name
y : [Name]
_ -> Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
y Integer
0 Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing Inerts
is
[] -> case [Bound] -> [Bound] -> Maybe (Maybe Integer, Maybe Integer)
boundInterval [Bound]
lbs [Bound]
ubs of
Maybe (Maybe Integer, Maybe Integer)
Nothing -> String -> Solutions
forall a. HasCallStack => String -> a
error String
"bug: cannot compute interval?"
Just (Maybe Integer
lb,Maybe Integer
ub) ->
let v :: Integer
v = Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe Integer
0 (Maybe Integer -> Maybe Integer -> Maybe Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus Maybe Integer
lb Maybe Integer
ub)
in Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
x Integer
v Maybe Integer
lb Maybe Integer
ub (Inerts -> Solutions) -> Inerts -> Solutions
forall a b. (a -> b) -> a -> b
$ Inerts
is { bounds :: NameMap ([Bound], [Bound])
bounds = NameMap ([Bound], [Bound])
mp1 }
slnEnumerate :: Solutions -> [ Solutions ]
slnEnumerate :: Solutions -> [Solutions]
slnEnumerate Solutions
s0 = Solutions -> [Solutions] -> [Solutions]
go Solutions
s0 []
where
go :: Solutions -> [Solutions] -> [Solutions]
go Solutions
s [Solutions]
k = case Solutions -> Maybe Solutions
slnNextVar Solutions
s of
Maybe Solutions
Nothing -> Solutions -> [Solutions] -> [Solutions]
hor Solutions
s [Solutions]
k
Just Solutions
s1 -> Solutions -> [Solutions] -> [Solutions]
go Solutions
s1 ([Solutions] -> [Solutions]) -> [Solutions] -> [Solutions]
forall a b. (a -> b) -> a -> b
$ case Solutions -> Maybe Solutions
slnNextVal Solutions
s of
Maybe Solutions
Nothing -> [Solutions]
k
Just Solutions
s2 -> Solutions -> [Solutions] -> [Solutions]
go Solutions
s2 [Solutions]
k
hor :: Solutions -> [Solutions] -> [Solutions]
hor Solutions
s [Solutions]
k = Solutions
s
Solutions -> [Solutions] -> [Solutions]
forall a. a -> [a] -> [a]
: case Solutions -> Maybe Solutions
slnNextVal Solutions
s of
Maybe Solutions
Nothing -> [Solutions]
k
Just Solutions
s1 -> Solutions -> [Solutions] -> [Solutions]
hor Solutions
s1 [Solutions]
k
slnNextVal :: Solutions -> Maybe Solutions
slnNextVal :: Solutions -> Maybe Solutions
slnNextVal Solutions
Done = Maybe Solutions
forall a. Maybe a
Nothing
slnNextVal (FixedVar Name
x Integer
v Solutions
i) = Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Solutions -> Maybe Solutions
slnNextVal Solutions
i
slnNextVal it :: Solutions
it@(TopVar Name
_ Integer
_ Maybe Integer
lb Maybe Integer
_ Inerts
_) =
case Maybe Integer
lb of
Just Integer
_ -> (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Solutions
it
Maybe Integer
Nothing -> (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract Integer
1) Solutions
it
slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith :: (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith Integer -> Integer
_ Solutions
Done = Maybe Solutions
forall a. Maybe a
Nothing
slnNextValWith Integer -> Integer
f (FixedVar Name
x Integer
v Solutions
i) = Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Integer -> Integer) -> Solutions -> Maybe Solutions
slnNextValWith Integer -> Integer
f Solutions
i
slnNextValWith Integer -> Integer
f (TopVar Name
x Integer
v Maybe Integer
lb Maybe Integer
ub Inerts
is) =
do let v1 :: Integer
v1 = Integer -> Integer
f Integer
v
case Maybe Integer
lb of
Just Integer
l -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
v1)
Maybe Integer
Nothing -> () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
case Maybe Integer
ub of
Just Integer
u -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
v1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
u)
Maybe Integer
Nothing -> () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Solutions -> Maybe Solutions
forall (m :: * -> *) a. Monad m => a -> m a
return (Solutions -> Maybe Solutions) -> Solutions -> Maybe Solutions
forall a b. (a -> b) -> a -> b
$ Name
-> Integer -> Maybe Integer -> Maybe Integer -> Inerts -> Solutions
TopVar Name
x Integer
v1 Maybe Integer
lb Maybe Integer
ub Inerts
is
slnNextVar :: Solutions -> Maybe Solutions
slnNextVar :: Solutions -> Maybe Solutions
slnNextVar Solutions
Done = Maybe Solutions
forall a. Maybe a
Nothing
slnNextVar (TopVar Name
x Integer
v Maybe Integer
_ Maybe Integer
_ Inerts
is) = Solutions -> Maybe Solutions
forall a. a -> Maybe a
Just (Solutions -> Maybe Solutions) -> Solutions -> Maybe Solutions
forall a b. (a -> b) -> a -> b
$ Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Solutions -> Solutions
forall a b. (a -> b) -> a -> b
$ Inerts -> Solutions
startIter (Inerts -> Solutions) -> Inerts -> Solutions
forall a b. (a -> b) -> a -> b
$ Name -> Integer -> Inerts -> Inerts
iLet Name
x Integer
v Inerts
is
slnNextVar (FixedVar Name
x Integer
v Solutions
i) = Name -> Integer -> Solutions -> Solutions
FixedVar Name
x Integer
v (Solutions -> Solutions) -> Maybe Solutions -> Maybe Solutions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Solutions -> Maybe Solutions
slnNextVar Solutions
i
iPickBounded :: BoundType -> [Bound] -> Maybe Integer
iPickBounded :: BoundType -> [Bound] -> Maybe Integer
iPickBounded BoundType
_ [] = Maybe Integer
forall a. Maybe a
Nothing
iPickBounded BoundType
bt [Bound]
bs =
do [Integer]
xs <- (Bound -> Maybe Integer) -> [Bound] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BoundType -> Bound -> Maybe Integer
normBound BoundType
bt) [Bound]
bs
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ case BoundType
bt of
BoundType
Lower -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Integer]
xs
BoundType
Upper -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
xs
where
normBound :: BoundType -> Bound -> Maybe Integer
normBound BoundType
Lower (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
k Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
normBound BoundType
Upper (Bound Integer
c Term
t) = do Integer
k <- Term -> Maybe Integer
isConst Term
t
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
kInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) Integer
c)
iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt (T Integer
k NameMap Integer
xs) Inerts
is = do [Integer]
ks <- ((Name, Integer) -> Maybe Integer)
-> [(Name, Integer)] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Integer) -> Maybe Integer
summand (NameMap Integer -> [(Name, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
xs)
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
k Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
ks
where
summand :: (Name, Integer) -> Maybe Integer
summand (Name
x,Integer
c) = (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) (BoundType -> Name -> Inerts -> Maybe Integer
iVarBound (Integer -> BoundType
forall a. (Ord a, Num a) => a -> BoundType
newBt Integer
c) Name
x Inerts
is)
newBt :: a -> BoundType
newBt a
c = if a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 then BoundType
bt else case BoundType
bt of
BoundType
Lower -> BoundType
Upper
BoundType
Upper -> BoundType
Lower
iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
iVarBound BoundType
bt Name
x Inerts
is
| Just Term
t <- Name -> NameMap Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Inerts -> NameMap Term
solved Inerts
is) = BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt Term
t Inerts
is
iVarBound BoundType
bt Name
x Inerts
is =
do ([Bound], [Bound])
both <- Name -> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
is)
case (Bound -> Maybe Integer) -> [Bound] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Bound -> Maybe Integer
fromBound (([Bound], [Bound]) -> [Bound]
forall b. (b, b) -> b
chooseBounds ([Bound], [Bound])
both) of
[] -> Maybe Integer
forall a. Maybe a
Nothing
[Integer]
bs -> Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return ([Integer] -> Integer
combineBounds [Integer]
bs)
where
fromBound :: Bound -> Maybe Integer
fromBound (Bound Integer
c Term
t) = (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
scaleBound Integer
c) (BoundType -> Term -> Inerts -> Maybe Integer
iTermBound BoundType
bt Term
t Inerts
is)
combineBounds :: [Integer] -> Integer
combineBounds = case BoundType
bt of
BoundType
Upper -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum
BoundType
Lower -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
chooseBounds :: (b, b) -> b
chooseBounds = case BoundType
bt of
BoundType
Upper -> (b, b) -> b
forall a b. (a, b) -> b
snd
BoundType
Lower -> (b, b) -> b
forall a b. (a, b) -> a
fst
scaleBound :: a -> a -> a
scaleBound a
c a
b = case BoundType
bt of
BoundType
Upper -> a -> a -> a
forall a. Integral a => a -> a -> a
div (a
ba -> a -> a
forall a. Num a => a -> a -> a
-a
1) a
c
BoundType
Lower -> a -> a -> a
forall a. Integral a => a -> a -> a
div a
b a
c a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
iModel :: Inerts -> [(Name,Integer)]
iModel :: Inerts -> [(Name, Integer)]
iModel Inerts
i = [(Name, Integer)]
-> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
goBounds [] (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
i)
where
goBounds :: [(Name, Integer)]
-> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
goBounds [(Name, Integer)]
su NameMap ([Bound], [Bound])
mp =
case NameMap ([Bound], [Bound])
-> Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey NameMap ([Bound], [Bound])
mp of
Maybe ((Name, ([Bound], [Bound])), NameMap ([Bound], [Bound]))
Nothing -> [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
goEqs [(Name, Integer)]
su ([(Name, Term)] -> [(Name, Integer)])
-> [(Name, Term)] -> [(Name, Integer)]
forall a b. (a -> b) -> a -> b
$ NameMap Term -> [(Name, Term)]
forall k a. Map k a -> [(k, a)]
Map.toList (NameMap Term -> [(Name, Term)]) -> NameMap Term -> [(Name, Term)]
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap Term
solved Inerts
i
Just ((Name
x,([Bound]
lbs0,[Bound]
ubs0)), NameMap ([Bound], [Bound])
mp1) ->
let lbs :: [Bound]
lbs = [ Integer -> Term -> Bound
Bound Integer
c ([(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
su Term
t) | Bound Integer
c Term
t <- [Bound]
lbs0 ]
ubs :: [Bound]
ubs = [ Integer -> Term -> Bound
Bound Integer
c ([(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
su Term
t) | Bound Integer
c Term
t <- [Bound]
ubs0 ]
sln :: Integer
sln = Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe Integer
0
(Maybe Integer -> Integer) -> Maybe Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Maybe Integer -> Maybe Integer -> Maybe Integer
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (BoundType -> [Bound] -> Maybe Integer
iPickBounded BoundType
Lower [Bound]
lbs) (BoundType -> [Bound] -> Maybe Integer
iPickBounded BoundType
Upper [Bound]
ubs)
in [(Name, Integer)]
-> NameMap ([Bound], [Bound]) -> [(Name, Integer)]
goBounds ((Name
x,Integer
sln) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: [(Name, Integer)]
su) NameMap ([Bound], [Bound])
mp1
goEqs :: [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
goEqs [(Name, Integer)]
su [] = [(Name, Integer)]
su
goEqs [(Name, Integer)]
su ((Name
x,Term
t) : [(Name, Term)]
more) =
let t1 :: Term
t1 = [(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
su Term
t
vs :: [Name]
vs = Term -> [Name]
tVarList Term
t1
su1 :: [(Name, Integer)]
su1 = [ (Name
v,Integer
0) | Name
v <- [Name]
vs ] [(Name, Integer)] -> [(Name, Integer)] -> [(Name, Integer)]
forall a. [a] -> [a] -> [a]
++ (Name
x,Term -> Integer
tConstPart Term
t1) (Name, Integer) -> [(Name, Integer)] -> [(Name, Integer)]
forall a. a -> [a] -> [a]
: [(Name, Integer)]
su
in [(Name, Integer)] -> [(Name, Term)] -> [(Name, Integer)]
goEqs [(Name, Integer)]
su1 [(Name, Term)]
more
solveIs0 :: Term -> S ()
solveIs0 :: Term -> S ()
solveIs0 Term
t = Term -> S ()
solveIs0' (Term -> S ()) -> S Term -> S ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> S Term
apSubst Term
t
solveIs0' :: Term -> S ()
solveIs0' :: Term -> S ()
solveIs0' Term
t
| Just Integer
a <- Term -> Maybe Integer
isConst Term
t = Bool -> S ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
| Just (Integer
a,Integer
b,Name
x) <- Term -> Maybe (Integer, Integer, Name)
tIsOneVar Term
t =
case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (-Integer
a) Integer
b of
(Integer
q,Integer
0) -> Name -> Term -> S ()
addDef Name
x (Integer -> Term
tConst Integer
q)
(Integer, Integer)
_ -> S ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
| Just (Integer
xc,Name
x,Term
s) <- Term -> Maybe (Integer, Name, Term)
tGetSimpleCoeff Term
t =
Name -> Term -> S ()
addDef Name
x (if Integer
xc Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 then Term -> Term
tNeg Term
s else Term
s)
| 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 = Integer -> Integer
forall a. Num a => a -> a
abs Integer
ak Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
Name
v <- S Name
newVar
let sgn :: Integer
sgn = Integer -> Integer
forall a. Num a => a -> a
signum Integer
ak
soln :: Term
soln = (Integer -> Integer
forall a. Num a => a -> a
negate Integer
sgn Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Integer -> Term -> Term
|*| Name -> Term
tVar Name
v
Term -> Term -> Term
|+| (Integer -> Integer) -> Term -> Term
tMapCoeff (\Integer
c -> Integer
sgn Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer -> Integer -> Integer
modulus Integer
c Integer
m) Term
s
Name -> Term -> S ()
addDef Name
xk Term
soln
let upd :: Integer -> Integer
upd Integer
i = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) (Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
m) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
modulus Integer
i Integer
m
Term -> S ()
solveIs0 (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer
forall a. Num a => a -> a
abs Integer
ak) Integer -> Term -> Term
|*| Name -> Term
tVar Name
v Term -> Term -> Term
|+| (Integer -> Integer) -> Term -> Term
tMapCoeff Integer -> Integer
upd Term
s)
| Bool
otherwise = String -> S ()
forall a. HasCallStack => String -> a
error String
"solveIs0: unreachable"
modulus :: Integer -> Integer -> Integer
modulus :: Integer -> Integer -> Integer
modulus Integer
a Integer
m = Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m)
solveIsNeg :: Term -> S ()
solveIsNeg :: Term -> S ()
solveIsNeg Term
t = Term -> S ()
solveIsNeg' (Term -> S ()) -> S Term -> S ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> S Term
apSubst Term
t
solveIsNeg' :: Term -> S ()
solveIsNeg' :: Term -> S ()
solveIsNeg' Term
t
| Just Integer
a <- Term -> Maybe Integer
isConst Term
t = Bool -> S ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)
| 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 Integer -> Integer -> Bool
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 = Integer -> Integer
forall a. Num a => a -> a
negate Integer
xc
beta :: Term
beta = Term
s
BoundType -> Name -> Bound -> S ()
addBound BoundType
Lower Name
x (Integer -> Term -> Bound
Bound Integer
b Term
beta)
[(Integer, Term, Integer, Term)]
-> S [(Integer, Term, Integer, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Integer
a,Term
alpha,Integer
b,Term
beta) | Bound Integer
a Term
alpha <- [Bound]
ubs ]
else do [Bound]
lbs <- BoundType -> Name -> S [Bound]
getBounds BoundType
Lower Name
x
let a :: Integer
a = Integer
xc
alpha :: Term
alpha = Term -> Term
tNeg Term
s
BoundType -> Name -> Bound -> S ()
addBound BoundType
Upper Name
x (Integer -> Term -> Bound
Bound Integer
a Term
alpha)
[(Integer, Term, Integer, Term)]
-> S [(Integer, Term, Integer, Term)]
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Integer
a,Term
alpha,Integer
b,Term
beta) | Bound Integer
b Term
beta <- [Bound]
lbs ]
((Integer, Term, Integer, Term) -> S ())
-> [(Integer, Term, Integer, Term)] -> S ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Integer
a,Term
alpha,Integer
b,Term
beta) ->
do let real :: Term
real = Term -> Term -> Term
ctLt (Integer
a Integer -> Term -> Term
|*| Term
beta) (Integer
b Integer -> Term -> Term
|*| Term
alpha)
dark :: Term
dark = Term -> Term -> Term
ctLt (Integer -> Term
tConst (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b)) (Integer
b Integer -> Term -> Term
|*| Term
alpha Term -> Term -> Term
|-| Integer
a Integer -> Term -> Term
|*| Term
beta)
gray :: [Term]
gray = [ Term -> Term -> Term
ctEq (Integer
b Integer -> Term -> Term
|*| Name -> Term
tVar Name
x) (Integer -> Term
tConst Integer
i Term -> Term -> Term
|+| Term
beta)
| Integer
i <- [ Integer
1 .. Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 ] ]
Term -> S ()
solveIsNeg Term
real
(S () -> S () -> S ()) -> S () -> [S ()] -> S ()
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl S () -> S () -> S ()
orElse (Term -> S ()
solveIsNeg Term
dark) ((Term -> S ()) -> [Term] -> [S ()]
forall a b. (a -> b) -> [a] -> [b]
map Term -> S ()
solveIs0 [Term]
gray)
) [(Integer, Term, Integer, Term)]
ctrs
| Bool
otherwise = String -> S ()
forall a. HasCallStack => String -> a
error String
"solveIsNeg: unreachable"
orElse :: S () -> S () -> S ()
orElse :: S () -> S () -> S ()
orElse S ()
x S ()
y = S () -> S () -> S ()
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus S ()
x S ()
y
data Answer a = None | One a | Choice (Answer a) (Answer a)
deriving Int -> Answer a -> ShowS
[Answer a] -> ShowS
Answer a -> String
(Int -> Answer a -> ShowS)
-> (Answer a -> String) -> ([Answer a] -> ShowS) -> Show (Answer a)
forall a. Show a => Int -> Answer a -> ShowS
forall a. Show a => [Answer a] -> ShowS
forall a. Show a => Answer a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Answer a] -> ShowS
$cshowList :: forall a. Show a => [Answer a] -> ShowS
show :: Answer a -> String
$cshow :: forall a. Show a => Answer a -> String
showsPrec :: Int -> Answer a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Answer a -> ShowS
Show
answerSize :: Answer a -> (Integer,Integer,Integer)
answerSize :: Answer a -> (Integer, Integer, Integer)
answerSize = Integer
-> Integer -> Integer -> Answer a -> (Integer, Integer, Integer)
forall t t t a.
(Num t, Num t, Num t) =>
t -> t -> t -> Answer a -> (t, t, t)
go Integer
0 Integer
0 Integer
0
where
go :: t -> t -> t -> Answer a -> (t, t, t)
go !t
n !t
o !t
c Answer a
ans =
case Answer a
ans of
Answer a
None -> (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1, t
o, t
c)
One a
_ -> (t
n, t
o t -> t -> t
forall a. Num a => a -> a -> a
+ t
1, t
c)
Choice Answer a
x Answer a
y ->
case t -> t -> t -> Answer a -> (t, t, t)
go t
n t
o (t
ct -> t -> t
forall a. Num a => a -> a -> a
+t
1) Answer a
x of
(t
n',t
o',t
c') -> t -> t -> t -> Answer a -> (t, t, t)
go t
n' t
o' t
c' Answer a
y
dotAnswer :: (a -> Doc) -> Answer a -> Doc
dotAnswer :: (a -> Doc) -> Answer a -> Doc
dotAnswer a -> Doc
pp Answer a
g0 = [Doc] -> Doc
vcat [String -> Doc
text String
"digraph {", Int -> Doc -> Doc
nest Int
2 ((Doc, Integer) -> Doc
forall a b. (a, b) -> a
fst ((Doc, Integer) -> Doc) -> (Doc, Integer) -> Doc
forall a b. (a -> b) -> a -> b
$ Integer -> Answer a -> (Doc, Integer)
go Integer
0 Answer a
g0), String -> Doc
text String
"}"]
where
node :: Integer -> a -> Doc
node Integer
x a
d = Integer -> Doc
integer Integer
x Doc -> Doc -> Doc
<+> Doc -> Doc
brackets (String -> Doc
text String
"label=" Doc -> Doc -> Doc
<> String -> Doc
text (a -> String
forall a. Show a => a -> String
show a
d))
Doc -> Doc -> Doc
<> Doc
semi
edge :: Integer -> Integer -> Doc
edge Integer
x Integer
y = Integer -> Doc
integer Integer
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
y
go :: Integer -> Answer a -> (Doc, Integer)
go Integer
x Answer a
None = let x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
in Integer -> (Doc, Integer) -> (Doc, Integer)
seq Integer
x' ( Integer -> String -> Doc
forall a. Show a => Integer -> a -> Doc
node Integer
x String
"", Integer
x' )
go Integer
x (One a
a) = let x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
in Integer -> (Doc, Integer) -> (Doc, Integer)
seq Integer
x' ( Integer -> String -> Doc
forall a. Show a => Integer -> a -> Doc
node Integer
x (Doc -> String
forall a. Show a => a -> String
show (a -> Doc
pp a
a)), Integer
x' )
go Integer
x (Choice Answer a
c1 Answer a
c2) = let x' :: Integer
x' = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
(Doc
ls1,Integer
x1) = Integer -> Answer a -> (Doc, Integer)
go Integer
x' Answer a
c1
(Doc
ls2,Integer
x2) = Integer -> Answer a -> (Doc, Integer)
go Integer
x1 Answer a
c2
in Integer -> (Doc, Integer) -> (Doc, Integer)
seq Integer
x'
( [Doc] -> Doc
vcat [ Integer -> String -> Doc
forall a. Show a => Integer -> a -> Doc
node Integer
x String
"|"
, Integer -> Integer -> Doc
edge Integer
x Integer
x'
, Integer -> Integer -> Doc
edge Integer
x Integer
x1
, Doc
ls1
, Doc
ls2
], Integer
x2 )
toList :: Answer a -> [a]
toList :: Answer a -> [a]
toList Answer a
a = Answer a -> [a] -> [a]
forall a. Answer a -> [a] -> [a]
go Answer a
a []
where
go :: Answer a -> [a] -> [a]
go (Choice Answer a
xs Answer a
ys) [a]
zs = Answer a -> [a] -> [a]
go Answer a
xs (Answer a -> [a] -> [a]
go Answer a
ys [a]
zs)
go (One a
x) [a]
xs = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs
go Answer a
None [a]
xs = [a]
xs
instance Monad Answer where
return :: a -> Answer a
return a
a = a -> Answer a
forall a. a -> Answer a
One a
a
#if !MIN_VERSION_ghc(8,8,1)
fail _ = None
#endif
Answer a
None >>= :: Answer a -> (a -> Answer b) -> Answer b
>>= a -> Answer b
_ = Answer b
forall a. Answer a
None
One a
a >>= a -> Answer b
k = a -> Answer b
k a
a
Choice Answer a
m1 Answer a
m2 >>= a -> Answer b
k = Answer b -> Answer b -> Answer b
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (Answer a
m1 Answer a -> (a -> Answer b) -> Answer b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Answer b
k) (Answer a
m2 Answer a -> (a -> Answer b) -> Answer b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Answer b
k)
instance Alternative Answer where
empty :: Answer a
empty = Answer a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
<|> :: Answer a -> Answer a -> Answer a
(<|>) = Answer a -> Answer a -> Answer a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
instance MonadPlus Answer where
mzero :: Answer a
mzero = Answer a
forall a. Answer a
None
mplus :: Answer a -> Answer a -> Answer a
mplus Answer a
None Answer a
x = Answer a
x
mplus Answer a
x Answer a
y = Answer a -> Answer a -> Answer a
forall a. Answer a -> Answer a -> Answer a
Choice Answer a
x Answer a
y
instance Functor Answer where
fmap :: (a -> b) -> Answer a -> Answer b
fmap a -> b
_ Answer a
None = Answer b
forall a. Answer a
None
fmap a -> b
f (One a
x) = b -> Answer b
forall a. a -> Answer a
One (a -> b
f a
x)
fmap a -> b
f (Choice Answer a
x1 Answer a
x2) = Answer b -> Answer b -> Answer b
forall a. Answer a -> Answer a -> Answer a
Choice ((a -> b) -> Answer a -> Answer b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Answer a
x1) ((a -> b) -> Answer a -> Answer b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Answer a
x2)
instance Applicative Answer where
pure :: a -> Answer a
pure = a -> Answer a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: Answer (a -> b) -> Answer a -> Answer b
(<*>) = Answer (a -> b) -> Answer a -> Answer b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
newtype S a = S (RW -> Answer (a,RW))
instance Monad S where
return :: a -> S a
return a
a = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
s -> (a, RW) -> Answer (a, RW)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a,RW
s)
S RW -> Answer (a, RW)
m >>= :: S a -> (a -> S b) -> S b
>>= a -> S b
k = (RW -> Answer (b, RW)) -> S b
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (b, RW)) -> S b) -> (RW -> Answer (b, RW)) -> S b
forall a b. (a -> b) -> a -> b
$ \RW
s -> do (a
a,RW
s1) <- RW -> Answer (a, RW)
m RW
s
let S RW -> Answer (b, RW)
m1 = a -> S b
k a
a
RW -> Answer (b, RW)
m1 RW
s1
instance Alternative S where
empty :: S a
empty = S a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
<|> :: S a -> S a -> S a
(<|>) = S a -> S a -> S a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
instance MonadPlus S where
mzero :: S a
mzero = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
_ -> Answer (a, RW)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
mplus :: S a -> S a -> S a
mplus (S RW -> Answer (a, RW)
m1) (S RW -> Answer (a, RW)
m2) = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
s -> Answer (a, RW) -> Answer (a, RW) -> Answer (a, RW)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (RW -> Answer (a, RW)
m1 RW
s) (RW -> Answer (a, RW)
m2 RW
s)
instance Functor S where
fmap :: (a -> b) -> S a -> S b
fmap = (a -> b) -> S a -> S b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Applicative S where
pure :: a -> S a
pure = a -> S a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: S (a -> b) -> S a -> S b
(<*>) = S (a -> b) -> S a -> S b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
updS :: (RW -> (a,RW)) -> S a
updS :: (RW -> (a, RW)) -> S a
updS RW -> (a, RW)
f = (RW -> Answer (a, RW)) -> S a
forall a. (RW -> Answer (a, RW)) -> S a
S ((RW -> Answer (a, RW)) -> S a) -> (RW -> Answer (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
s -> (a, RW) -> Answer (a, RW)
forall (m :: * -> *) a. Monad m => a -> m a
return (RW -> (a, RW)
f RW
s)
updS_ :: (RW -> RW) -> S ()
updS_ :: (RW -> RW) -> S ()
updS_ RW -> RW
f = (RW -> ((), RW)) -> S ()
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> ((), RW)) -> S ()) -> (RW -> ((), RW)) -> S ()
forall a b. (a -> b) -> a -> b
$ \RW
rw -> ((),RW -> RW
f RW
rw)
get :: (RW -> a) -> S a
get :: (RW -> a) -> S a
get RW -> a
f = (RW -> (a, RW)) -> S a
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> (a, RW)) -> S a) -> (RW -> (a, RW)) -> S a
forall a b. (a -> b) -> a -> b
$ \RW
rw -> (RW -> a
f RW
rw, RW
rw)
newVar :: S Name
newVar :: S Name
newVar = (RW -> (Name, RW)) -> S Name
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> (Name, RW)) -> S Name) -> (RW -> (Name, RW)) -> S Name
forall a b. (a -> b) -> a -> b
$ \RW
rw -> ( Int -> Name
SysName (RW -> Int
nameSource RW
rw)
, RW
rw { nameSource :: Int
nameSource = RW -> Int
nameSource RW
rw Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 }
)
getBounds :: BoundType -> Name -> S [Bound]
getBounds :: BoundType -> Name -> S [Bound]
getBounds BoundType
f Name
x = (RW -> [Bound]) -> S [Bound]
forall a. (RW -> a) -> S a
get ((RW -> [Bound]) -> S [Bound]) -> (RW -> [Bound]) -> S [Bound]
forall a b. (a -> b) -> a -> b
$ \RW
rw -> case Name -> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound]))
-> NameMap ([Bound], [Bound]) -> Maybe ([Bound], [Bound])
forall a b. (a -> b) -> a -> b
$ Inerts -> NameMap ([Bound], [Bound])
bounds (Inerts -> NameMap ([Bound], [Bound]))
-> Inerts -> NameMap ([Bound], [Bound])
forall a b. (a -> b) -> a -> b
$ RW -> Inerts
inerts RW
rw of
Maybe ([Bound], [Bound])
Nothing -> []
Just ([Bound], [Bound])
bs -> case BoundType
f of
BoundType
Lower -> ([Bound], [Bound]) -> [Bound]
forall a b. (a, b) -> a
fst ([Bound], [Bound])
bs
BoundType
Upper -> ([Bound], [Bound]) -> [Bound]
forall a b. (a, b) -> b
snd ([Bound], [Bound])
bs
addBound :: BoundType -> Name -> Bound -> S ()
addBound :: BoundType -> Name -> Bound -> S ()
addBound BoundType
bt Name
x Bound
b = (RW -> RW) -> S ()
updS_ ((RW -> RW) -> S ()) -> (RW -> RW) -> S ()
forall a b. (a -> b) -> a -> b
$ \RW
rw ->
let i :: Inerts
i = RW -> Inerts
inerts RW
rw
entry :: ([Bound], [Bound])
entry = case BoundType
bt of
BoundType
Lower -> ([Bound
b],[])
BoundType
Upper -> ([],[Bound
b])
jn :: ([a], [a]) -> ([a], [a]) -> ([a], [a])
jn ([a]
newL,[a]
newU) ([a]
oldL,[a]
oldU) = ([a]
newL[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
oldL, [a]
newU[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
oldU)
in RW
rw { inerts :: Inerts
inerts = Inerts
i { bounds :: NameMap ([Bound], [Bound])
bounds = (([Bound], [Bound]) -> ([Bound], [Bound]) -> ([Bound], [Bound]))
-> Name
-> ([Bound], [Bound])
-> NameMap ([Bound], [Bound])
-> NameMap ([Bound], [Bound])
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith ([Bound], [Bound]) -> ([Bound], [Bound]) -> ([Bound], [Bound])
forall a a. ([a], [a]) -> ([a], [a]) -> ([a], [a])
jn Name
x ([Bound], [Bound])
entry (Inerts -> NameMap ([Bound], [Bound])
bounds Inerts
i) }}
addDef :: Name -> Term -> S ()
addDef :: Name -> Term -> S ()
addDef Name
x Term
t =
do [Term]
newWork <- (RW -> ([Term], RW)) -> S [Term]
forall a. (RW -> (a, RW)) -> S a
updS ((RW -> ([Term], RW)) -> S [Term])
-> (RW -> ([Term], RW)) -> S [Term]
forall a b. (a -> b) -> a -> b
$ \RW
rw -> let ([Term]
newWork,Inerts
newInerts) = Name -> Term -> Inerts -> ([Term], Inerts)
iSolved Name
x Term
t (RW -> Inerts
inerts RW
rw)
in ([Term]
newWork, RW
rw { inerts :: Inerts
inerts = Inerts
newInerts })
(Term -> S ()) -> [Term] -> S ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Term -> S ()
solveIsNeg [Term]
newWork
apSubst :: Term -> S Term
apSubst :: Term -> S Term
apSubst Term
t =
do Inerts
i <- (RW -> Inerts) -> S Inerts
forall a. (RW -> a) -> S a
get RW -> Inerts
inerts
Term -> S Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Inerts -> Term -> Term
iApSubst Inerts
i Term
t)
data Name = UserName !Int | SysName !Int
deriving (ReadPrec [Name]
ReadPrec Name
Int -> ReadS Name
ReadS [Name]
(Int -> ReadS Name)
-> ReadS [Name] -> ReadPrec Name -> ReadPrec [Name] -> Read Name
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Name]
$creadListPrec :: ReadPrec [Name]
readPrec :: ReadPrec Name
$creadPrec :: ReadPrec Name
readList :: ReadS [Name]
$creadList :: ReadS [Name]
readsPrec :: Int -> ReadS Name
$creadsPrec :: Int -> ReadS Name
Read,Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show,Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq,Eq Name
Eq Name
-> (Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord)
ppName :: Name -> Doc
ppName :: Name -> Doc
ppName (UserName Int
x) = String -> Doc
text String
"u" Doc -> Doc -> Doc
<> Int -> Doc
int Int
x
ppName (SysName Int
x) = String -> Doc
text String
"s" Doc -> Doc -> Doc
<> Int -> Doc
int Int
x
toName :: Int -> Name
toName :: Int -> Name
toName = Int -> Name
UserName
fromName :: Name -> Maybe Int
fromName :: Name -> Maybe Int
fromName (UserName Int
x) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
x
fromName (SysName Int
_) = Maybe Int
forall a. Maybe a
Nothing
type NameMap = Map Name
data Term = T !Integer (NameMap Integer)
deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq,Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord)
infixl 6 |+|, |-|
infixr 7 |*|
tConst :: Integer -> Term
tConst :: Integer -> Term
tConst Integer
k = Integer -> NameMap Integer -> Term
T Integer
k NameMap Integer
forall k a. Map k a
Map.empty
tVar :: Name -> Term
tVar :: Name -> Term
tVar Name
x = Integer -> NameMap Integer -> Term
T Integer
0 (Name -> Integer -> NameMap Integer
forall k a. k -> a -> Map k a
Map.singleton Name
x Integer
1)
(|+|) :: Term -> Term -> Term
T Integer
n1 NameMap Integer
m1 |+| :: Term -> Term -> Term
|+| T Integer
n2 NameMap Integer
m2 = Integer -> NameMap Integer -> Term
T (Integer
n1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n2)
(NameMap Integer -> Term) -> NameMap Integer -> Term
forall a b. (a -> b) -> a -> b
$ if NameMap Integer -> Bool
forall k a. Map k a -> Bool
Map.null NameMap Integer
m1 then NameMap Integer
m2 else
if NameMap Integer -> Bool
forall k a. Map k a -> Bool
Map.null NameMap Integer
m2 then NameMap Integer
m1 else
(Integer -> Bool) -> NameMap Integer -> NameMap Integer
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) (NameMap Integer -> NameMap Integer)
-> NameMap Integer -> NameMap Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer)
-> NameMap Integer -> NameMap Integer -> NameMap Integer
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) NameMap Integer
m1 NameMap Integer
m2
(|*|) :: Integer -> Term -> Term
Integer
0 |*| :: Integer -> Term -> Term
|*| Term
_ = Integer -> Term
tConst Integer
0
Integer
1 |*| Term
t = Term
t
Integer
k |*| T Integer
n NameMap Integer
m = Integer -> NameMap Integer -> Term
T (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
n) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*) NameMap Integer
m)
tNeg :: Term -> Term
tNeg :: Term -> Term
tNeg Term
t = (-Integer
1) Integer -> Term -> Term
|*| Term
t
(|-|) :: Term -> Term -> Term
Term
t1 |-| :: Term -> Term -> Term
|-| Term
t2 = Term
t1 Term -> Term -> Term
|+| Term -> Term
tNeg Term
t2
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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) NameMap Integer
m
tLetNums :: [(Name,Integer)] -> Term -> Term
tLetNums :: [(Name, Integer)] -> Term -> Term
tLetNums [(Name, Integer)]
xs Term
t = ((Name, Integer) -> Term -> Term)
-> Term -> [(Name, Integer)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
x,Integer
i) Term
t1 -> Name -> Integer -> Term -> Term
tLetNum Name
x Integer
i Term
t1) Term
t [(Name, Integer)]
xs
instance Show Term where
showsPrec :: Int -> Term -> ShowS
showsPrec Int
c Term
t = Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
c (Doc -> String
forall a. Show a => a -> String
show (Term -> Doc
ppTerm Term
t))
ppTerm :: Term -> Doc
ppTerm :: Term -> Doc
ppTerm (T Integer
k NameMap Integer
m) =
case NameMap Integer -> [(Name, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
m of
[] -> Integer -> Doc
integer Integer
k
[(Name, Integer)]
xs | Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 -> [Doc] -> Doc
hsep (Integer -> Doc
integer Integer
k Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Name, Integer) -> Doc) -> [(Name, Integer)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Integer) -> Doc
ppProd [(Name, Integer)]
xs)
(Name, Integer)
x : [(Name, Integer)]
xs -> [Doc] -> Doc
hsep ((Name, Integer) -> Doc
ppFst (Name, Integer)
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Name, Integer) -> Doc) -> [(Name, Integer)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Integer) -> Doc
ppProd [(Name, Integer)]
xs)
where
ppFst :: (Name, Integer) -> Doc
ppFst (Name
x,Integer
1) = Name -> Doc
ppName Name
x
ppFst (Name
x,-1) = String -> Doc
text String
"-" Doc -> Doc -> Doc
<> Name -> Doc
ppName Name
x
ppFst (Name
x,Integer
n) = Integer -> Name -> Doc
ppMul Integer
n Name
x
ppProd :: (Name, Integer) -> Doc
ppProd (Name
x,Integer
1) = String -> Doc
text String
"+" Doc -> Doc -> Doc
<+> Name -> Doc
ppName Name
x
ppProd (Name
x,-1) = String -> Doc
text String
"-" Doc -> Doc -> Doc
<+> Name -> Doc
ppName Name
x
ppProd (Name
x,Integer
n) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = String -> Doc
text String
"+" Doc -> Doc -> Doc
<+> Integer -> Name -> Doc
ppMul Integer
n Name
x
| Bool
otherwise = String -> Doc
text String
"-" Doc -> Doc -> Doc
<+> Integer -> Name -> Doc
ppMul (Integer -> Integer
forall a. Num a => a -> a
abs Integer
n) Name
x
ppMul :: Integer -> Name -> Doc
ppMul Integer
n Name
x = Integer -> Doc
integer Integer
n Doc -> Doc -> Doc
<+> String -> Doc
text String
"*" Doc -> Doc -> Doc
<+> Name -> Doc
ppName Name
x
tSplitVar :: Name -> Term -> (Integer, Term)
tSplitVar :: Name -> Term -> (Integer, Term)
tSplitVar Name
x t :: Term
t@(T Integer
n NameMap Integer
m) =
case (Name -> Integer -> Maybe Integer)
-> Name -> NameMap Integer -> (Maybe Integer, NameMap Integer)
forall k a.
Ord k =>
(k -> a -> Maybe a) -> k -> Map k a -> (Maybe a, Map k a)
Map.updateLookupWithKey (\Name
_ Integer
_ -> Maybe Integer
forall a. Maybe a
Nothing) Name
x NameMap Integer
m of
(Maybe Integer
Nothing,NameMap Integer
_) -> (Integer
0,Term
t)
(Just Integer
k,NameMap Integer
m1) -> (Integer
k, Integer -> NameMap Integer -> Term
T Integer
n NameMap Integer
m1)
tHasVar :: Name -> Term -> Bool
tHasVar :: Name -> Term -> Bool
tHasVar Name
x (T Integer
_ NameMap Integer
m) = Name -> NameMap Integer -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Name
x NameMap Integer
m
isConst :: Term -> Maybe Integer
isConst :: Term -> Maybe Integer
isConst (T Integer
n NameMap Integer
m)
| NameMap Integer -> Bool
forall k a. Map k a -> Bool
Map.null NameMap Integer
m = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
| Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing
tConstPart :: Term -> Integer
tConstPart :: Term -> Integer
tConstPart (T Integer
n NameMap Integer
_) = Integer
n
tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
tIsOneVar (T Integer
a NameMap Integer
m) = case NameMap Integer -> [(Name, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList NameMap Integer
m of
[ (Name
x,Integer
b) ] -> (Integer, Integer, Name) -> Maybe (Integer, Integer, Name)
forall a. a -> Maybe a
Just (Integer
a, Integer
b, Name
x)
[(Name, Integer)]
_ -> Maybe (Integer, Integer, Name)
forall a. Maybe a
Nothing
tGetSimpleCoeff :: Term -> Maybe (Integer, Name, Term)
tGetSimpleCoeff :: Term -> Maybe (Integer, Name, Term)
tGetSimpleCoeff (T Integer
a NameMap Integer
m) =
do let (NameMap Integer
m1,NameMap Integer
m2) = (Integer -> Bool)
-> NameMap Integer -> (NameMap Integer, NameMap Integer)
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partition (\Integer
x -> Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 Bool -> Bool -> Bool
|| Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -Integer
1) NameMap Integer
m
((Name
x,Integer
xc), NameMap Integer
m3) <- NameMap Integer -> Maybe ((Name, Integer), NameMap Integer)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey NameMap Integer
m1
(Integer, Name, Term) -> Maybe (Integer, Name, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
xc, Name
x, Integer -> NameMap Integer -> Term
T Integer
a (NameMap Integer -> NameMap Integer -> NameMap Integer
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union NameMap Integer
m3 NameMap Integer
m2))
tVarList :: Term -> [Name]
tVarList :: Term -> [Name]
tVarList (T Integer
_ NameMap Integer
m) = NameMap Integer -> [Name]
forall k a. Map k a -> [k]
Map.keys NameMap Integer
m
tFactor :: Term -> Maybe (Integer, Term)
tFactor :: Term -> Maybe (Integer, Term)
tFactor (T Integer
c NameMap Integer
m) =
do Integer
d <- [Integer] -> Maybe Integer
common (Integer
c Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: NameMap Integer -> [Integer]
forall k a. Map k a -> [a]
Map.elems NameMap Integer
m)
(Integer, Term) -> Maybe (Integer, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
d, Integer -> NameMap Integer -> Term
T (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
c Integer
d) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d) NameMap Integer
m))
where
common :: [Integer] -> Maybe Integer
common :: [Integer] -> Maybe Integer
common [] = Maybe Integer
forall a. Maybe a
Nothing
common [Integer
x] = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
x
common (Integer
x : Integer
y : [Integer]
zs) =
case Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
x Integer
y of
Integer
1 -> Maybe Integer
forall a. Maybe a
Nothing
Integer
n -> [Integer] -> Maybe Integer
common (Integer
n Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
zs)
tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)
tLeastAbsCoeff :: Term -> Maybe (Integer, Name, Term)
tLeastAbsCoeff (T Integer
c NameMap Integer
m) = do (Integer
xc,Name
x,NameMap Integer
m1) <- (Name
-> Integer
-> Maybe (Integer, Name, NameMap Integer)
-> Maybe (Integer, Name, NameMap Integer))
-> Maybe (Integer, Name, NameMap Integer)
-> NameMap Integer
-> Maybe (Integer, Name, NameMap Integer)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Name
-> Integer
-> Maybe (Integer, Name, NameMap Integer)
-> Maybe (Integer, Name, NameMap Integer)
forall a.
(Ord a, Num a) =>
Name
-> a
-> Maybe (a, Name, NameMap Integer)
-> Maybe (a, Name, NameMap Integer)
step Maybe (Integer, Name, NameMap Integer)
forall a. Maybe a
Nothing NameMap Integer
m
(Integer, Name, Term) -> Maybe (Integer, Name, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
xc, Name
x, Integer -> NameMap Integer -> Term
T Integer
c NameMap Integer
m1)
where
step :: Name
-> a
-> Maybe (a, Name, NameMap Integer)
-> Maybe (a, Name, NameMap Integer)
step Name
x a
xc Maybe (a, Name, NameMap Integer)
Nothing = (a, Name, NameMap Integer) -> Maybe (a, Name, NameMap Integer)
forall a. a -> Maybe a
Just (a
xc, Name
x, Name -> NameMap Integer -> NameMap Integer
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
x NameMap Integer
m)
step Name
x a
xc (Just (a
yc,Name
_,NameMap Integer
_))
| a -> a
forall a. Num a => a -> a
abs a
xc a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a -> a
forall a. Num a => a -> a
abs a
yc = (a, Name, NameMap Integer) -> Maybe (a, Name, NameMap Integer)
forall a. a -> Maybe a
Just (a
xc, Name
x, Name -> NameMap Integer -> NameMap Integer
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
x NameMap Integer
m)
step Name
_ a
_ Maybe (a, Name, NameMap Integer)
it = Maybe (a, Name, NameMap Integer)
it
tLeastVar :: Term -> Maybe (Integer, Name, Term)
tLeastVar :: Term -> Maybe (Integer, Name, Term)
tLeastVar (T Integer
c NameMap Integer
m) =
do ((Name
x,Integer
xc), NameMap Integer
m1) <- NameMap Integer -> Maybe ((Name, Integer), NameMap Integer)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey NameMap Integer
m
(Integer, Name, Term) -> Maybe (Integer, Name, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
xc, Name
x, Integer -> NameMap Integer -> Term
T Integer
c NameMap Integer
m1)
tMapCoeff :: (Integer -> Integer) -> Term -> Term
tMapCoeff :: (Integer -> Integer) -> Term -> Term
tMapCoeff Integer -> Integer
f (T Integer
c NameMap Integer
m) = Integer -> NameMap Integer -> Term
T (Integer -> Integer
f Integer
c) ((Integer -> Integer) -> NameMap Integer -> NameMap Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> Integer
f NameMap Integer
m)