{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.OrdRel
-- Copyright   :  (c) Masahiro Sakai 2011
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Ordering relations
--
-----------------------------------------------------------------------------
module ToySolver.Data.OrdRel
  (
  -- * Relational operators
    RelOp (..)
  , flipOp
  , negOp
  , showOp
  , evalOp

  -- * Relation
  , OrdRel (..)
  , fromOrdRel

  -- * DSL
  , IsEqRel (..)
  , IsOrdRel (..)
  ) where

import qualified Data.IntSet as IS

import ToySolver.Data.Boolean
import ToySolver.Data.IntVar

infix 4 .<., .<=., .>=., .>., .==., ./=.

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

-- | relational operators
data RelOp = Lt | Le | Ge | Gt | Eql | NEq
    deriving (Int -> RelOp -> ShowS
[RelOp] -> ShowS
RelOp -> String
(Int -> RelOp -> ShowS)
-> (RelOp -> String) -> ([RelOp] -> ShowS) -> Show RelOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RelOp -> ShowS
showsPrec :: Int -> RelOp -> ShowS
$cshow :: RelOp -> String
show :: RelOp -> String
$cshowList :: [RelOp] -> ShowS
showList :: [RelOp] -> ShowS
Show, RelOp -> RelOp -> Bool
(RelOp -> RelOp -> Bool) -> (RelOp -> RelOp -> Bool) -> Eq RelOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RelOp -> RelOp -> Bool
== :: RelOp -> RelOp -> Bool
$c/= :: RelOp -> RelOp -> Bool
/= :: RelOp -> RelOp -> Bool
Eq, Eq RelOp
Eq RelOp =>
(RelOp -> RelOp -> Ordering)
-> (RelOp -> RelOp -> Bool)
-> (RelOp -> RelOp -> Bool)
-> (RelOp -> RelOp -> Bool)
-> (RelOp -> RelOp -> Bool)
-> (RelOp -> RelOp -> RelOp)
-> (RelOp -> RelOp -> RelOp)
-> Ord RelOp
RelOp -> RelOp -> Bool
RelOp -> RelOp -> Ordering
RelOp -> RelOp -> RelOp
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
$ccompare :: RelOp -> RelOp -> Ordering
compare :: RelOp -> RelOp -> Ordering
$c< :: RelOp -> RelOp -> Bool
< :: RelOp -> RelOp -> Bool
$c<= :: RelOp -> RelOp -> Bool
<= :: RelOp -> RelOp -> Bool
$c> :: RelOp -> RelOp -> Bool
> :: RelOp -> RelOp -> Bool
$c>= :: RelOp -> RelOp -> Bool
>= :: RelOp -> RelOp -> Bool
$cmax :: RelOp -> RelOp -> RelOp
max :: RelOp -> RelOp -> RelOp
$cmin :: RelOp -> RelOp -> RelOp
min :: RelOp -> RelOp -> RelOp
Ord)


-- | flipping relational operator
--
-- @rel (flipOp op) a b@ is equivalent to @rel op b a@
flipOp :: RelOp -> RelOp
flipOp :: RelOp -> RelOp
flipOp RelOp
Le = RelOp
Ge
flipOp RelOp
Ge = RelOp
Le
flipOp RelOp
Lt = RelOp
Gt
flipOp RelOp
Gt = RelOp
Lt
flipOp RelOp
Eql = RelOp
Eql
flipOp RelOp
NEq = RelOp
NEq

-- | negating relational operator
--
-- @rel (negOp op) a b@ is equivalent to @notB (rel op a b)@
negOp :: RelOp -> RelOp
negOp :: RelOp -> RelOp
negOp RelOp
Lt = RelOp
Ge
negOp RelOp
Le = RelOp
Gt
negOp RelOp
Ge = RelOp
Lt
negOp RelOp
Gt = RelOp
Le
negOp RelOp
Eql = RelOp
NEq
negOp RelOp
NEq = RelOp
Eql

-- | operator symbol
showOp :: RelOp -> String
showOp :: RelOp -> String
showOp RelOp
Lt = String
"<"
showOp RelOp
Le = String
"<="
showOp RelOp
Ge = String
">="
showOp RelOp
Gt = String
">"
showOp RelOp
Eql = String
"="
showOp RelOp
NEq = String
"/="

-- | evaluate an operator into a comparision function
evalOp :: Ord a => RelOp -> a -> a -> Bool
evalOp :: forall a. Ord a => RelOp -> a -> a -> Bool
evalOp RelOp
Lt = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<)
evalOp RelOp
Le = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
evalOp RelOp
Ge = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
evalOp RelOp
Gt = a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>)
evalOp RelOp
Eql = a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
evalOp RelOp
NEq = a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(/=)

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

-- | type class for constructing relational formula
class IsEqRel e r | r -> e where
  (.==.) :: e -> e -> r
  (./=.) :: e -> e -> r

-- | type class for constructing relational formula
class IsEqRel e r => IsOrdRel e r | r -> e where
  (.<.), (.<=.), (.>.), (.>=.) :: e -> e -> r
  ordRel :: RelOp -> e -> e -> r

  e
a .<. e
b  = RelOp -> e -> e -> r
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
Lt e
a e
b
  e
a .<=. e
b = RelOp -> e -> e -> r
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
Le e
a e
b
  e
a .>. e
b  = RelOp -> e -> e -> r
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
Gt e
a e
b
  e
a .>=. e
b = RelOp -> e -> e -> r
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
Ge e
a e
b

  ordRel RelOp
Lt e
a e
b  = e
a e -> e -> r
forall e r. IsOrdRel e r => e -> e -> r
.<. e
b
  ordRel RelOp
Gt e
a e
b  = e
a e -> e -> r
forall e r. IsOrdRel e r => e -> e -> r
.>. e
b
  ordRel RelOp
Le e
a e
b  = e
a e -> e -> r
forall e r. IsOrdRel e r => e -> e -> r
.<=. e
b
  ordRel RelOp
Ge e
a e
b  = e
a e -> e -> r
forall e r. IsOrdRel e r => e -> e -> r
.>=. e
b
  ordRel RelOp
Eql e
a e
b = e
a e -> e -> r
forall e r. IsEqRel e r => e -> e -> r
.==. e
b
  ordRel RelOp
NEq e
a e
b = e
a e -> e -> r
forall e r. IsEqRel e r => e -> e -> r
./=. e
b

  {-# MINIMAL ((.<.), (.<=.), (.>.), (.>=.)) | ordRel #-}

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

-- | Atomic formula
data OrdRel e = OrdRel e RelOp e
    deriving (Int -> OrdRel e -> ShowS
[OrdRel e] -> ShowS
OrdRel e -> String
(Int -> OrdRel e -> ShowS)
-> (OrdRel e -> String) -> ([OrdRel e] -> ShowS) -> Show (OrdRel e)
forall e. Show e => Int -> OrdRel e -> ShowS
forall e. Show e => [OrdRel e] -> ShowS
forall e. Show e => OrdRel e -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall e. Show e => Int -> OrdRel e -> ShowS
showsPrec :: Int -> OrdRel e -> ShowS
$cshow :: forall e. Show e => OrdRel e -> String
show :: OrdRel e -> String
$cshowList :: forall e. Show e => [OrdRel e] -> ShowS
showList :: [OrdRel e] -> ShowS
Show, OrdRel e -> OrdRel e -> Bool
(OrdRel e -> OrdRel e -> Bool)
-> (OrdRel e -> OrdRel e -> Bool) -> Eq (OrdRel e)
forall e. Eq e => OrdRel e -> OrdRel e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall e. Eq e => OrdRel e -> OrdRel e -> Bool
== :: OrdRel e -> OrdRel e -> Bool
$c/= :: forall e. Eq e => OrdRel e -> OrdRel e -> Bool
/= :: OrdRel e -> OrdRel e -> Bool
Eq, Eq (OrdRel e)
Eq (OrdRel e) =>
(OrdRel e -> OrdRel e -> Ordering)
-> (OrdRel e -> OrdRel e -> Bool)
-> (OrdRel e -> OrdRel e -> Bool)
-> (OrdRel e -> OrdRel e -> Bool)
-> (OrdRel e -> OrdRel e -> Bool)
-> (OrdRel e -> OrdRel e -> OrdRel e)
-> (OrdRel e -> OrdRel e -> OrdRel e)
-> Ord (OrdRel e)
OrdRel e -> OrdRel e -> Bool
OrdRel e -> OrdRel e -> Ordering
OrdRel e -> OrdRel e -> OrdRel e
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 e. Ord e => Eq (OrdRel e)
forall e. Ord e => OrdRel e -> OrdRel e -> Bool
forall e. Ord e => OrdRel e -> OrdRel e -> Ordering
forall e. Ord e => OrdRel e -> OrdRel e -> OrdRel e
$ccompare :: forall e. Ord e => OrdRel e -> OrdRel e -> Ordering
compare :: OrdRel e -> OrdRel e -> Ordering
$c< :: forall e. Ord e => OrdRel e -> OrdRel e -> Bool
< :: OrdRel e -> OrdRel e -> Bool
$c<= :: forall e. Ord e => OrdRel e -> OrdRel e -> Bool
<= :: OrdRel e -> OrdRel e -> Bool
$c> :: forall e. Ord e => OrdRel e -> OrdRel e -> Bool
> :: OrdRel e -> OrdRel e -> Bool
$c>= :: forall e. Ord e => OrdRel e -> OrdRel e -> Bool
>= :: OrdRel e -> OrdRel e -> Bool
$cmax :: forall e. Ord e => OrdRel e -> OrdRel e -> OrdRel e
max :: OrdRel e -> OrdRel e -> OrdRel e
$cmin :: forall e. Ord e => OrdRel e -> OrdRel e -> OrdRel e
min :: OrdRel e -> OrdRel e -> OrdRel e
Ord)

instance Complement (OrdRel c) where
  notB :: OrdRel c -> OrdRel c
notB (OrdRel c
lhs RelOp
op c
rhs) = c -> RelOp -> c -> OrdRel c
forall e. e -> RelOp -> e -> OrdRel e
OrdRel c
lhs (RelOp -> RelOp
negOp RelOp
op) c
rhs

instance IsEqRel e (OrdRel e) where
  .==. :: e -> e -> OrdRel e
(.==.) = RelOp -> e -> e -> OrdRel e
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
Eql
  ./=. :: e -> e -> OrdRel e
(./=.) = RelOp -> e -> e -> OrdRel e
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
NEq

instance IsOrdRel e (OrdRel e) where
  ordRel :: RelOp -> e -> e -> OrdRel e
ordRel RelOp
op e
a e
b = e -> RelOp -> e -> OrdRel e
forall e. e -> RelOp -> e -> OrdRel e
OrdRel e
a RelOp
op e
b

instance Variables e => Variables (OrdRel e) where
  vars :: OrdRel e -> VarSet
vars (OrdRel e
a RelOp
_ e
b) = e -> VarSet
forall a. Variables a => a -> VarSet
vars e
a VarSet -> VarSet -> VarSet
`IS.union` e -> VarSet
forall a. Variables a => a -> VarSet
vars e
b

instance Functor OrdRel where
  fmap :: forall a b. (a -> b) -> OrdRel a -> OrdRel b
fmap a -> b
f (OrdRel a
a RelOp
op a
b) = b -> RelOp -> b -> OrdRel b
forall e. e -> RelOp -> e -> OrdRel e
OrdRel (a -> b
f a
a) RelOp
op (a -> b
f a
b)

fromOrdRel :: IsOrdRel e r => OrdRel e -> r
fromOrdRel :: forall e r. IsOrdRel e r => OrdRel e -> r
fromOrdRel (OrdRel e
a RelOp
op e
b) = RelOp -> e -> e -> r
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
op e
a e
b

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

instance (Eval m e a, Ord a) => Eval m (OrdRel e) Bool where
  eval :: m -> OrdRel e -> Bool
eval m
m (OrdRel e
lhs RelOp
op e
rhs) = RelOp -> a -> a -> Bool
forall a. Ord a => RelOp -> a -> a -> Bool
evalOp RelOp
op (m -> e -> a
forall m e v. Eval m e v => m -> e -> v
eval m
m e
lhs) (m -> e -> a
forall m e v. Eval m e v => m -> e -> v
eval m
m e
rhs)