{-# 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' <- 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

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