{-# OPTIONS_GHC -Wall #-}
module ToySolver.Data.LA.FOL
( fromFOLAtom
, toFOLFormula
, fromFOLExpr
, toFOLExpr
) where
import Control.Monad
import Data.VectorSpace
import ToySolver.Data.OrdRel
import ToySolver.Data.FOL.Arith
import qualified ToySolver.Data.LA as LA
fromFOLAtom :: (Real r, Fractional r) => Atom r -> Maybe (LA.Atom r)
fromFOLAtom :: forall r. (Real r, Fractional r) => Atom r -> Maybe (Atom r)
fromFOLAtom (OrdRel Expr r
a RelOp
op Expr r
b) = do
Expr r
a' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a
Expr r
b' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
b
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
op Expr r
a' Expr r
b'
toFOLFormula :: (Real r) => LA.Atom r -> Formula (Atom r)
toFOLFormula :: forall r. Real r => Atom r -> Formula (Atom r)
toFOLFormula Atom r
r = forall a. a -> Formula a
Atom forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall r. Real r => Expr r -> Expr r
toFOLExpr Atom r
r
fromFOLExpr :: (Real r, Fractional r) => Expr r -> Maybe (LA.Expr r)
fromFOLExpr :: forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr (Const r
c) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall r. (Num r, Eq r) => r -> Expr r
LA.constant r
c)
fromFOLExpr (Var Var
v) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall r. Num r => Var -> Expr r
LA.var Var
v)
fromFOLExpr (Expr r
a :+: Expr r
b) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall v. AdditiveGroup v => v -> v -> v
(^+^) (forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a) (forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
b)
fromFOLExpr (Expr r
a :*: Expr r
b) = do
Expr r
a' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a
Expr r
b' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
b
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ do{ r
c <- forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
a'; forall (m :: * -> *) a. Monad m => a -> m a
return (r
c forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
b') }
, do{ r
c <- forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
b'; forall (m :: * -> *) a. Monad m => a -> m a
return (r
c forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
a') }
]
fromFOLExpr (Expr r
a :/: Expr r
b) = do
Expr r
a' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a
Expr r
b' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
b
r
c <- forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
b'
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ r
c forall a. Eq a => a -> a -> Bool
/= r
0
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr r
a' forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/ r
c)
toFOLExpr :: (Real r) => LA.Expr r -> Expr r
toFOLExpr :: forall r. Real r => Expr r -> Expr r
toFOLExpr Expr r
e =
case forall a b. (a -> b) -> [a] -> [b]
map forall {r}. Num r => (r, Var) -> Expr r
f (forall r. Expr r -> [(r, Var)]
LA.terms Expr r
e) of
[] -> forall r. r -> Expr r
Const r
0
[Expr r
t] -> Expr r
t
[Expr r]
ts -> forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall a. Num a => a -> a -> a
(+) [Expr r]
ts
where
f :: (r, Var) -> Expr r
f (r
c,Var
x)
| Var
x forall a. Eq a => a -> a -> Bool
== Var
LA.unitVar = forall r. r -> Expr r
Const r
c
| Bool
otherwise = forall r. r -> Expr r
Const r
c forall a. Num a => a -> a -> a
* forall r. Var -> Expr r
Var Var
x