{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
module ToySolver.Data.LA
(
Expr
, Var
, var
, constant
, terms
, fromTerms
, coeffMap
, fromCoeffMap
, unitVar
, asConst
, coeff
, lookupCoeff
, extract
, extractMaybe
, mapCoeff
, mapCoeffWithVar
, evalLinear
, lift1
, applySubst
, applySubst1
, showExpr
, Atom (..)
, showAtom
, applySubstAtom
, applySubst1Atom
, solveFor
, module ToySolver.Data.OrdRel
, Eval (..)
, BoundsEnv
, computeInterval
) where
import Control.Monad
import Control.DeepSeq
import Data.List
import Data.Maybe
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import qualified Data.IntSet as IntSet
import Data.Interval
import Data.VectorSpace
import qualified ToySolver.Data.OrdRel as OrdRel
import ToySolver.Data.OrdRel
import ToySolver.Data.IntVar
newtype Expr r
= Expr
{
forall r. Expr r -> IntMap r
coeffMap :: IntMap r
} deriving (Expr r -> Expr r -> Bool
forall r. Eq r => Expr r -> Expr r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr r -> Expr r -> Bool
$c/= :: forall r. Eq r => Expr r -> Expr r -> Bool
== :: Expr r -> Expr r -> Bool
$c== :: forall r. Eq r => Expr r -> Expr r -> Bool
Eq, Expr r -> Expr r -> Bool
Expr r -> Expr r -> Ordering
Expr r -> Expr r -> Expr r
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
forall {r}. Ord r => Eq (Expr r)
forall r. Ord r => Expr r -> Expr r -> Bool
forall r. Ord r => Expr r -> Expr r -> Ordering
forall r. Ord r => Expr r -> Expr r -> Expr r
min :: Expr r -> Expr r -> Expr r
$cmin :: forall r. Ord r => Expr r -> Expr r -> Expr r
max :: Expr r -> Expr r -> Expr r
$cmax :: forall r. Ord r => Expr r -> Expr r -> Expr r
>= :: Expr r -> Expr r -> Bool
$c>= :: forall r. Ord r => Expr r -> Expr r -> Bool
> :: Expr r -> Expr r -> Bool
$c> :: forall r. Ord r => Expr r -> Expr r -> Bool
<= :: Expr r -> Expr r -> Bool
$c<= :: forall r. Ord r => Expr r -> Expr r -> Bool
< :: Expr r -> Expr r -> Bool
$c< :: forall r. Ord r => Expr r -> Expr r -> Bool
compare :: Expr r -> Expr r -> Ordering
$ccompare :: forall r. Ord r => Expr r -> Expr r -> Ordering
Ord)
fromCoeffMap :: (Num r, Eq r) => IntMap r -> Expr r
fromCoeffMap :: forall r. (Num r, Eq r) => IntMap r -> Expr r
fromCoeffMap IntMap r
m = forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr (forall r. IntMap r -> Expr r
Expr IntMap r
m)
terms :: Expr r -> [(r,Var)]
terms :: forall r. Expr r -> [(r, Var)]
terms (Expr IntMap r
m) = [(r
c,Var
v) | (Var
v,r
c) <- forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m]
fromTerms :: (Num r, Eq r) => [(r,Var)] -> Expr r
fromTerms :: forall r. (Num r, Eq r) => [(r, Var)] -> Expr r
fromTerms [(r, Var)]
ts = forall r. (Num r, Eq r) => IntMap r -> Expr r
fromCoeffMap forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> [(Var, a)] -> IntMap a
IntMap.fromListWith forall a. Num a => a -> a -> a
(+) [(Var
x,r
c) | (r
c,Var
x) <- [(r, Var)]
ts]
instance Variables (Expr r) where
vars :: Expr r -> VarSet
vars (Expr IntMap r
m) = Var -> VarSet -> VarSet
IntSet.delete Var
unitVar (forall a. IntMap a -> VarSet
IntMap.keysSet IntMap r
m)
instance Show r => Show (Expr r) where
showsPrec :: Var -> Expr r -> ShowS
showsPrec Var
d Expr r
m = Bool -> ShowS -> ShowS
showParen (Var
d forall a. Ord a => a -> a -> Bool
> Var
10) forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"fromTerms " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ShowS
shows (forall r. Expr r -> [(r, Var)]
terms Expr r
m)
instance (Num r, Eq r, Read r) => Read (Expr r) where
readsPrec :: Var -> ReadS (Expr r)
readsPrec Var
p = forall a. Bool -> ReadS a -> ReadS a
readParen (Var
p forall a. Ord a => a -> a -> Bool
> Var
10) forall a b. (a -> b) -> a -> b
$ \ String
r -> do
(String
"fromTerms",String
s) <- ReadS String
lex String
r
([(r, Var)]
xs,String
t) <- forall a. Read a => ReadS a
reads String
s
forall (m :: * -> *) a. Monad m => a -> m a
return (forall r. (Num r, Eq r) => [(r, Var)] -> Expr r
fromTerms [(r, Var)]
xs, String
t)
instance NFData r => NFData (Expr r) where
rnf :: Expr r -> ()
rnf (Expr IntMap r
m) = forall a. NFData a => a -> ()
rnf IntMap r
m
unitVar :: Var
unitVar :: Var
unitVar = -Var
1
asConst :: Num r => Expr r -> Maybe r
asConst :: forall r. Num r => Expr r -> Maybe r
asConst (Expr IntMap r
m) =
case forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m of
[] -> forall a. a -> Maybe a
Just r
0
[(Var
v,r
x)] | Var
vforall a. Eq a => a -> a -> Bool
==Var
unitVar -> forall a. a -> Maybe a
Just r
x
[(Var, r)]
_ -> forall a. Maybe a
Nothing
normalizeExpr :: (Num r, Eq r) => Expr r -> Expr r
normalizeExpr :: forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr (Expr IntMap r
t) = forall r. IntMap r -> Expr r
Expr forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> IntMap a -> IntMap a
IntMap.filter (r
0forall a. Eq a => a -> a -> Bool
/=) IntMap r
t
var :: Num r => Var -> Expr r
var :: forall r. Num r => Var -> Expr r
var Var
v = forall r. IntMap r -> Expr r
Expr forall a b. (a -> b) -> a -> b
$ forall a. Var -> a -> IntMap a
IntMap.singleton Var
v r
1
constant :: (Num r, Eq r) => r -> Expr r
constant :: forall r. (Num r, Eq r) => r -> Expr r
constant r
c = forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr forall a b. (a -> b) -> a -> b
$ forall r. IntMap r -> Expr r
Expr forall a b. (a -> b) -> a -> b
$ forall a. Var -> a -> IntMap a
IntMap.singleton Var
unitVar r
c
mapCoeff :: (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff :: forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff a -> b
f (Expr IntMap a
t) = forall r. IntMap r -> Expr r
Expr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe a -> Maybe b
g IntMap a
t
where
g :: a -> Maybe b
g a
c = if b
c' forall a. Eq a => a -> a -> Bool
== b
0 then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just b
c'
where c' :: b
c' = a -> b
f a
c
mapCoeffWithVar :: (Num b, Eq b) => (a -> Var -> b) -> Expr a -> Expr b
mapCoeffWithVar :: forall b a. (Num b, Eq b) => (a -> Var -> b) -> Expr a -> Expr b
mapCoeffWithVar a -> Var -> b
f (Expr IntMap a
t) = forall r. IntMap r -> Expr r
Expr forall a b. (a -> b) -> a -> b
$ forall a b. (Var -> a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybeWithKey Var -> a -> Maybe b
g IntMap a
t
where
g :: Var -> a -> Maybe b
g Var
v a
c = if b
c' forall a. Eq a => a -> a -> Bool
== b
0 then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just b
c'
where c' :: b
c' = a -> Var -> b
f a
c Var
v
instance (Num r, Eq r) => AdditiveGroup (Expr r) where
Expr IntMap r
t ^+^ :: Expr r -> Expr r -> Expr r
^+^ Expr r
e2 | forall a. IntMap a -> Bool
IntMap.null IntMap r
t = Expr r
e2
Expr r
e1 ^+^ Expr IntMap r
t | forall a. IntMap a -> Bool
IntMap.null IntMap r
t = Expr r
e1
Expr r
e1 ^+^ Expr r
e2 = forall r. (Num r, Eq r) => Expr r -> Expr r
normalizeExpr forall a b. (a -> b) -> a -> b
$ forall r. Num r => Expr r -> Expr r -> Expr r
plus Expr r
e1 Expr r
e2
zeroV :: Expr r
zeroV = forall r. IntMap r -> Expr r
Expr forall a b. (a -> b) -> a -> b
$ forall a. IntMap a
IntMap.empty
negateV :: Expr r -> Expr r
negateV = ((-r
1) forall v. VectorSpace v => Scalar v -> v -> v
*^)
instance (Num r, Eq r) => VectorSpace (Expr r) where
type Scalar (Expr r) = r
Scalar (Expr r)
1 *^ :: Scalar (Expr r) -> Expr r -> Expr r
*^ Expr r
e = Expr r
e
Scalar (Expr r)
0 *^ Expr r
e = forall v. AdditiveGroup v => v
zeroV
Scalar (Expr r)
c *^ Expr r
e = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff (Scalar (Expr r)
cforall a. Num a => a -> a -> a
*) Expr r
e
plus :: Num r => Expr r -> Expr r -> Expr r
plus :: forall r. Num r => Expr r -> Expr r -> Expr r
plus (Expr IntMap r
t1) (Expr IntMap r
t2) = forall r. IntMap r -> Expr r
Expr forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall a. Num a => a -> a -> a
(+) IntMap r
t1 IntMap r
t2
instance Num r => Eval (Model r) (Expr r) r where
eval :: Model r -> Expr r -> r
eval Model r
m (Expr Model r
t) = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [(Model r
m' forall a. IntMap a -> Var -> a
IntMap.! Var
v) forall a. Num a => a -> a -> a
* r
c | (Var
v,r
c) <- forall a. IntMap a -> [(Var, a)]
IntMap.toList Model r
t]
where m' :: Model r
m' = forall a. Var -> a -> IntMap a -> IntMap a
IntMap.insert Var
unitVar r
1 Model r
m
evalLinear :: VectorSpace a => Model a -> a -> Expr (Scalar a) -> a
evalLinear :: forall a. VectorSpace a => Model a -> a -> Expr (Scalar a) -> a
evalLinear Model a
m a
u (Expr IntMap (Scalar a)
t) = forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Scalar a
c forall v. VectorSpace v => Scalar v -> v -> v
*^ (Model a
m' forall a. IntMap a -> Var -> a
IntMap.! Var
v) | (Var
v,Scalar a
c) <- forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap (Scalar a)
t]
where m' :: Model a
m' = forall a. Var -> a -> IntMap a -> IntMap a
IntMap.insert Var
unitVar a
u Model a
m
lift1 :: VectorSpace x => x -> (Var -> x) -> Expr (Scalar x) -> x
lift1 :: forall x. VectorSpace x => x -> (Var -> x) -> Expr (Scalar x) -> x
lift1 x
unit Var -> x
f (Expr IntMap (Scalar x)
t) = forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Scalar x
c forall v. VectorSpace v => Scalar v -> v -> v
*^ (Var -> x
g Var
v) | (Var
v,Scalar x
c) <- forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap (Scalar x)
t]
where
g :: Var -> x
g Var
v
| Var
vforall a. Eq a => a -> a -> Bool
==Var
unitVar = x
unit
| Bool
otherwise = Var -> x
f Var
v
applySubst :: (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst :: forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst VarMap (Expr r)
s (Expr IntMap r
m) = forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV (forall a b. (a -> b) -> [a] -> [b]
map (Var, r) -> Expr r
f (forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m))
where
f :: (Var, r) -> Expr r
f (Var
v,r
c) = r
c forall v. VectorSpace v => Scalar v -> v -> v
*^ (
case forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
v VarMap (Expr r)
s of
Just Expr r
tm -> Expr r
tm
Maybe (Expr r)
Nothing -> forall r. Num r => Var -> Expr r
var Var
v)
applySubst1 :: (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 :: forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 Var
x Expr r
e Expr r
e1 =
case forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe Var
x Expr r
e1 of
Maybe (r, Expr r)
Nothing -> Expr r
e1
Just (r
c,Expr r
e2) -> r
c forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
e forall v. AdditiveGroup v => v -> v -> v
^+^ Expr r
e2
coeff :: Num r => Var -> Expr r -> r
coeff :: forall r. Num r => Var -> Expr r -> r
coeff Var
v (Expr IntMap r
m) = forall a. a -> Var -> IntMap a -> a
IntMap.findWithDefault r
0 Var
v IntMap r
m
lookupCoeff :: Num r => Var -> Expr r -> Maybe r
lookupCoeff :: forall r. Num r => Var -> Expr r -> Maybe r
lookupCoeff Var
v (Expr IntMap r
m) = forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
v IntMap r
m
extract :: Num r => Var -> Expr r -> (r, Expr r)
Var
v (Expr IntMap r
m) = (forall a. a -> Var -> IntMap a -> a
IntMap.findWithDefault r
0 Var
v IntMap r
m, forall r. IntMap r -> Expr r
Expr (forall a. Var -> IntMap a -> IntMap a
IntMap.delete Var
v IntMap r
m))
extractMaybe :: Num r => Var -> Expr r -> Maybe (r, Expr r)
Var
v (Expr IntMap r
m) =
case forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
v IntMap r
m of
Maybe r
Nothing -> forall a. Maybe a
Nothing
Just r
c -> forall a. a -> Maybe a
Just (r
c, forall r. IntMap r -> Expr r
Expr (forall a. Var -> IntMap a -> IntMap a
IntMap.delete Var
v IntMap r
m))
showExpr :: (Num r, Eq r, Show r) => Expr r -> String
showExpr :: forall r. (Num r, Eq r, Show r) => Expr r -> String
showExpr = forall r.
(Num r, Show r, Eq r) =>
(Var -> String) -> Expr r -> String
showExprWith forall {a}. Show a => a -> String
f
where
f :: a -> String
f a
x = String
"x" forall a. [a] -> [a] -> [a]
++ forall {a}. Show a => a -> String
show a
x
showExprWith :: (Num r, Show r, Eq r) => (Var -> String) -> Expr r -> String
showExprWith :: forall r.
(Num r, Show r, Eq r) =>
(Var -> String) -> Expr r -> String
showExprWith Var -> String
env (Expr IntMap r
m) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id [ShowS]
xs String
""
where
xs :: [ShowS]
xs = forall a. a -> [a] -> [a]
intersperse (String -> ShowS
showString String
" + ") [ShowS]
ts
ts :: [ShowS]
ts = [if r
cforall a. Eq a => a -> a -> Bool
==r
1
then String -> ShowS
showString (Var -> String
env Var
x)
else forall a. Show a => Var -> a -> ShowS
showsPrec Var
8 r
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"*" forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (Var -> String
env Var
x)
| (Var
x,r
c) <- forall a. IntMap a -> [(Var, a)]
IntMap.toList IntMap r
m, Var
x forall a. Eq a => a -> a -> Bool
/= Var
unitVar] forall a. [a] -> [a] -> [a]
++
[forall a. Show a => Var -> a -> ShowS
showsPrec Var
7 r
c | r
c <- forall a. Maybe a -> [a]
maybeToList (forall a. Var -> IntMap a -> Maybe a
IntMap.lookup Var
unitVar IntMap r
m)]
type Atom r = OrdRel (Expr r)
showAtom :: (Num r, Eq r, Show r) => Atom r -> String
showAtom :: forall r. (Num r, Eq r, Show r) => Atom r -> String
showAtom (OrdRel Expr r
lhs RelOp
op Expr r
rhs) = forall r. (Num r, Eq r, Show r) => Expr r -> String
showExpr Expr r
lhs forall a. [a] -> [a] -> [a]
++ RelOp -> String
showOp RelOp
op forall a. [a] -> [a] -> [a]
++ forall r. (Num r, Eq r, Show r) => Expr r -> String
showExpr Expr r
rhs
applySubstAtom :: (Num r, Eq r) => VarMap (Expr r) -> Atom r -> Atom r
applySubstAtom :: forall r. (Num r, Eq r) => VarMap (Expr r) -> Atom r -> Atom r
applySubstAtom VarMap (Expr r)
s (OrdRel Expr r
lhs RelOp
op Expr r
rhs) = forall e. e -> RelOp -> e -> OrdRel e
OrdRel (forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst VarMap (Expr r)
s Expr r
lhs) RelOp
op (forall r. (Num r, Eq r) => VarMap (Expr r) -> Expr r -> Expr r
applySubst VarMap (Expr r)
s Expr r
rhs)
applySubst1Atom :: (Num r, Eq r) => Var -> Expr r -> Atom r -> Atom r
applySubst1Atom :: forall r. (Num r, Eq r) => Var -> Expr r -> Atom r -> Atom r
applySubst1Atom Var
x Expr r
e (OrdRel Expr r
lhs RelOp
op Expr r
rhs) = forall e. e -> RelOp -> e -> OrdRel e
OrdRel (forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 Var
x Expr r
e Expr r
lhs) RelOp
op (forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
applySubst1 Var
x Expr r
e Expr r
rhs)
solveFor :: (Real r, Fractional r) => Atom r -> Var -> Maybe (RelOp, Expr r)
solveFor :: forall r.
(Real r, Fractional r) =>
Atom r -> Var -> Maybe (RelOp, Expr r)
solveFor (OrdRel Expr r
lhs RelOp
op Expr r
rhs) Var
v = do
(r
c,Expr r
e) <- forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe Var
v (Expr r
lhs forall v. AdditiveGroup v => v -> v -> v
^-^ Expr r
rhs)
forall (m :: * -> *) a. Monad m => a -> m a
return ( if r
c forall a. Ord a => a -> a -> Bool
< r
0 then RelOp -> RelOp
flipOp RelOp
op else RelOp
op
, (r
1forall a. Fractional a => a -> a -> a
/r
c) forall v. VectorSpace v => Scalar v -> v -> v
*^ forall v. AdditiveGroup v => v -> v
negateV Expr r
e
)
type BoundsEnv r = VarMap (Interval r)
computeInterval :: (Real r, Fractional r) => BoundsEnv r -> Expr r -> Interval r
computeInterval :: forall r.
(Real r, Fractional r) =>
BoundsEnv r -> Expr r -> Interval r
computeInterval BoundsEnv r
b = forall m e v. Eval m e v => m -> e -> v
eval BoundsEnv r
b forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
mapCoeff forall r. Ord r => r -> Interval r
Data.Interval.singleton