{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.LA
-- Copyright   :  (c) Masahiro Sakai 2011
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Some definition for Theory of Linear Arithmetics.
--
-----------------------------------------------------------------------------
module ToySolver.Data.LA
  (
  -- * Expression of linear arithmetics
    Expr
  , Var

  -- ** Conversion
  , var
  , constant
  , terms
  , fromTerms
  , coeffMap
  , fromCoeffMap
  , unitVar
  , asConst

  -- ** Query
  , coeff
  , lookupCoeff
  , extract
  , extractMaybe

  -- ** Operations
  , mapCoeff
  , mapCoeffWithVar
  , evalLinear
  , lift1
  , applySubst
  , applySubst1
  , showExpr

  -- * Atomic formula of linear arithmetics
  , Atom (..)
  , showAtom
  , applySubstAtom
  , applySubst1Atom
  , solveFor
  , module ToySolver.Data.OrdRel

  -- * Evaluation of expression and atomic formula
  , Eval (..)

  -- * misc
  , 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

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

-- | Linear combination of variables and constants.
-- Non-negative keys are used for variables's coefficients.
-- key 'unitVar' is used for constants.
newtype Expr r
  = Expr
  { -- | a mapping from variables to coefficients
    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)

-- | Create a @Expr@ from a mapping from variables to coefficients.
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 contained in the expression.
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]

-- | Create a @Expr@ from a list of terms.
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

-- | Special variable that should always be evaluated to 1.
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

-- | variable
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
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

-- | map coefficients.
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

-- | map coefficients.
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

-- | evaluate the expression under the model.
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 x e e1 == e1[e/x]
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

-- | lookup a coefficient of the variable.
-- @
--   coeff v e == fst (extract v e)
-- @
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

-- | lookup a coefficient of the variable.
-- It returns @Nothing@ if the expression does not contain @v@.
-- @
--   lookupCoeff v e == fmap fst (extractMaybe v e)
-- @
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 v e@ returns @(c, e')@ such that @e == c *^ v ^+^ e'@
extract :: Num r => Var -> Expr r -> (r, Expr r)
extract :: forall r. Num r => Var -> Expr r -> (r, Expr r)
extract 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))
{-
-- Alternative implementation which may be faster but allocte more memory
extract v (Expr m) =
  case IntMap.updateLookupWithKey (\_ _ -> Nothing) v m of
    (Nothing, _) -> (0, Expr m)
    (Just c, m2) -> (c, Expr m2)
-}

-- | @extractMaybe v e@ returns @Just (c, e')@ such that @e == c *^ v ^+^ e'@
-- if @e@ contains v, and returns @Nothing@ otherwise.
extractMaybe :: Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe :: forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
extractMaybe 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))
{-
-- Alternative implementation which may be faster but allocte more memory
extractMaybe v (Expr m) =
  case IntMap.updateLookupWithKey (\_ _ -> Nothing) v m of
    (Nothing, _) -> Nothing
    (Just c, m2) -> Just (c, Expr m2)
-}

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)]

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

-- | Atomic Formula of Linear Arithmetics
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)

-- | applySubst1 x e phi == phi[e/x]
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)

-- | Solve linear (in)equation for the given variable.
--
-- @solveFor a v@ returns @Just (op, e)@ such that @Atom v op e@
-- is equivalent to @a@.
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)

-- | compute bounds for a @Expr@ with respect to @BoundsEnv@.
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

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