{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.LA.FOL
-- Copyright   :  (c) Masahiro Sakai 2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
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' <- Expr r -> Maybe (Expr r)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a
  Expr r
b' <- Expr r -> Maybe (Expr r)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
b
  Atom r -> Maybe (Atom r)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom r -> Maybe (Atom r)) -> Atom r -> Maybe (Atom r)
forall a b. (a -> b) -> a -> b
$ RelOp -> Expr r -> Expr r -> Atom r
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 = Atom r -> Formula (Atom r)
forall a. a -> Formula a
Atom (Atom r -> Formula (Atom r)) -> Atom r -> Formula (Atom r)
forall a b. (a -> b) -> a -> b
$ (Expr r -> Expr r) -> Atom r -> Atom r
forall a b. (a -> b) -> OrdRel a -> OrdRel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr r -> Expr r
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) = Expr r -> Maybe (Expr r)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> Expr r
forall r. (Num r, Eq r) => r -> Expr r
LA.constant r
c)
fromFOLExpr (Var Var
v)   = Expr r -> Maybe (Expr r)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Expr r
forall r. Num r => Var -> Expr r
LA.var Var
v)
fromFOLExpr (Expr r
a :+: Expr r
b) = (Expr r -> Expr r -> Expr r)
-> Maybe (Expr r) -> Maybe (Expr r) -> Maybe (Expr r)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Expr r -> Expr r -> Expr r
forall v. AdditiveGroup v => v -> v -> v
(^+^) (Expr r -> Maybe (Expr r)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a) (Expr r -> Maybe (Expr r)
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' <- Expr r -> Maybe (Expr r)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a
  Expr r
b' <- Expr r -> Maybe (Expr r)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
b
  [Maybe (Expr r)] -> Maybe (Expr r)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ do{ r
c <- Expr r -> Maybe r
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
a'; Expr r -> Maybe (Expr r)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (r
Scalar (Expr r)
c Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
b') }
       , do{ r
c <- Expr r -> Maybe r
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
b'; Expr r -> Maybe (Expr r)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (r
Scalar (Expr r)
c Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
a') }
       ]
fromFOLExpr (Expr r
a :/: Expr r
b) = do
  Expr r
a' <- Expr r -> Maybe (Expr r)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
a
  Expr r
b' <- Expr r -> Maybe (Expr r)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
fromFOLExpr Expr r
b
  r
c <- Expr r -> Maybe r
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
b'
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ r
c r -> r -> Bool
forall a. Eq a => a -> a -> Bool
/= r
0
  Expr r -> Maybe (Expr r)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr r
a' Expr r -> r -> Expr r
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 ((r, Var) -> Expr r) -> [(r, Var)] -> [Expr r]
forall a b. (a -> b) -> [a] -> [b]
map (r, Var) -> Expr r
forall {r}. Num r => (r, Var) -> Expr r
f (Expr r -> [(r, Var)]
forall r. Expr r -> [(r, Var)]
LA.terms Expr r
e) of
    []  -> r -> Expr r
forall r. r -> Expr r
Const r
0
    [Expr r
t] -> Expr r
t
    [Expr r]
ts  -> (Expr r -> Expr r -> Expr r) -> [Expr r] -> Expr r
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Expr r -> Expr r -> Expr r
forall a. Num a => a -> a -> a
(+) [Expr r]
ts
  where
    f :: (r, Var) -> Expr r
f (r
c,Var
x)
      | Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
LA.unitVar = r -> Expr r
forall r. r -> Expr r
Const r
c
      | Bool
otherwise       = r -> Expr r
forall r. r -> Expr r
Const r
c Expr r -> Expr r -> Expr r
forall a. Num a => a -> a -> a
* Var -> Expr r
forall r. Var -> Expr r
Var Var
x

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