{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}

module Language.REST.ConcreteOC where

import qualified Language.REST.OCAlgebra as AOC
import qualified Language.REST.Internal.WQO as WQO
import           Language.REST.RuntimeTerm
import           Language.REST.RPO
import           Language.REST.Op

import Data.Hashable
import GHC.Generics (Generic)
import qualified Data.Set as S

newtype ConcreteOC = ConcreteOC (S.Set (WQO.WQO Op))
  deriving (ConcreteOC -> ConcreteOC -> Bool
(ConcreteOC -> ConcreteOC -> Bool)
-> (ConcreteOC -> ConcreteOC -> Bool) -> Eq ConcreteOC
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConcreteOC -> ConcreteOC -> Bool
== :: ConcreteOC -> ConcreteOC -> Bool
$c/= :: ConcreteOC -> ConcreteOC -> Bool
/= :: ConcreteOC -> ConcreteOC -> Bool
Eq, Eq ConcreteOC
Eq ConcreteOC =>
(ConcreteOC -> ConcreteOC -> Ordering)
-> (ConcreteOC -> ConcreteOC -> Bool)
-> (ConcreteOC -> ConcreteOC -> Bool)
-> (ConcreteOC -> ConcreteOC -> Bool)
-> (ConcreteOC -> ConcreteOC -> Bool)
-> (ConcreteOC -> ConcreteOC -> ConcreteOC)
-> (ConcreteOC -> ConcreteOC -> ConcreteOC)
-> Ord ConcreteOC
ConcreteOC -> ConcreteOC -> Bool
ConcreteOC -> ConcreteOC -> Ordering
ConcreteOC -> ConcreteOC -> ConcreteOC
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 :: ConcreteOC -> ConcreteOC -> Ordering
compare :: ConcreteOC -> ConcreteOC -> Ordering
$c< :: ConcreteOC -> ConcreteOC -> Bool
< :: ConcreteOC -> ConcreteOC -> Bool
$c<= :: ConcreteOC -> ConcreteOC -> Bool
<= :: ConcreteOC -> ConcreteOC -> Bool
$c> :: ConcreteOC -> ConcreteOC -> Bool
> :: ConcreteOC -> ConcreteOC -> Bool
$c>= :: ConcreteOC -> ConcreteOC -> Bool
>= :: ConcreteOC -> ConcreteOC -> Bool
$cmax :: ConcreteOC -> ConcreteOC -> ConcreteOC
max :: ConcreteOC -> ConcreteOC -> ConcreteOC
$cmin :: ConcreteOC -> ConcreteOC -> ConcreteOC
min :: ConcreteOC -> ConcreteOC -> ConcreteOC
Ord, (forall x. ConcreteOC -> Rep ConcreteOC x)
-> (forall x. Rep ConcreteOC x -> ConcreteOC) -> Generic ConcreteOC
forall x. Rep ConcreteOC x -> ConcreteOC
forall x. ConcreteOC -> Rep ConcreteOC x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConcreteOC -> Rep ConcreteOC x
from :: forall x. ConcreteOC -> Rep ConcreteOC x
$cto :: forall x. Rep ConcreteOC x -> ConcreteOC
to :: forall x. Rep ConcreteOC x -> ConcreteOC
Generic, Eq ConcreteOC
Eq ConcreteOC =>
(Int -> ConcreteOC -> Int)
-> (ConcreteOC -> Int) -> Hashable ConcreteOC
Int -> ConcreteOC -> Int
ConcreteOC -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> ConcreteOC -> Int
hashWithSalt :: Int -> ConcreteOC -> Int
$chash :: ConcreteOC -> Int
hash :: ConcreteOC -> Int
Hashable)

instance Show ConcreteOC where
  show :: ConcreteOC -> String
show (ConcreteOC Set (WQO Op)
ords) = Int -> String
forall a. Show a => a -> String
show (Set (WQO Op) -> Int
forall a. Set a -> Int
S.size Set (WQO Op)
ords) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" orderings"

concreteOC :: Monad m => S.Set Op -> AOC.OCAlgebra ConcreteOC RuntimeTerm m
concreteOC :: forall (m :: * -> *).
Monad m =>
Set Op -> OCAlgebra ConcreteOC RuntimeTerm m
concreteOC Set Op
ops = (ConcreteOC -> m Bool)
-> (ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC)
-> ConcreteOC
-> (ConcreteOC -> ConcreteOC -> ConcreteOC)
-> (ConcreteOC -> ConcreteOC -> m Bool)
-> OCAlgebra ConcreteOC RuntimeTerm m
forall c a (m :: * -> *).
(c -> m Bool)
-> (c -> a -> a -> c)
-> c
-> (c -> c -> c)
-> (c -> c -> m Bool)
-> OCAlgebra c a m
AOC.OCAlgebra (Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> (ConcreteOC -> Bool) -> ConcreteOC -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcreteOC -> Bool
isSat) ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC
refine (Set (WQO Op) -> ConcreteOC
ConcreteOC (Set Op -> Set (WQO Op)
forall a. (Ord a, Eq a, Hashable a) => Set a -> Set (WQO a)
WQO.orderings Set Op
ops)) ConcreteOC -> ConcreteOC -> ConcreteOC
union ConcreteOC -> ConcreteOC -> m Bool
forall {m :: * -> *}. Monad m => ConcreteOC -> ConcreteOC -> m Bool
notStrongerThan
  where
    union :: ConcreteOC -> ConcreteOC -> ConcreteOC
union (ConcreteOC Set (WQO Op)
ord1) (ConcreteOC Set (WQO Op)
ord2) = Set (WQO Op) -> ConcreteOC
ConcreteOC (Set (WQO Op) -> ConcreteOC) -> Set (WQO Op) -> ConcreteOC
forall a b. (a -> b) -> a -> b
$ Set (WQO Op) -> Set (WQO Op) -> Set (WQO Op)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (WQO Op)
ord1 Set (WQO Op)
ord2
    notStrongerThan :: ConcreteOC -> ConcreteOC -> m Bool
notStrongerThan (ConcreteOC Set (WQO Op)
ord1) (ConcreteOC Set (WQO Op)
ord2) = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Set (WQO Op)
ord1 Set (WQO Op) -> Set (WQO Op) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (WQO Op)
ord2 Bool -> Bool -> Bool
|| Set (WQO Op)
ord2 Set (WQO Op) -> Set (WQO Op) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set (WQO Op)
ord1

    isSat :: ConcreteOC -> Bool
    isSat :: ConcreteOC -> Bool
isSat (ConcreteOC Set (WQO Op)
ords) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set (WQO Op) -> Bool
forall a. Set a -> Bool
S.null Set (WQO Op)
ords

    refine :: ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC
    refine :: ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC
refine (ConcreteOC Set (WQO Op)
ords) RuntimeTerm
t RuntimeTerm
u = Set (WQO Op) -> ConcreteOC
ConcreteOC ((WQO Op -> Bool) -> Set (WQO Op) -> Set (WQO Op)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (\WQO Op
ord -> WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE WQO Op
ord RuntimeTerm
t RuntimeTerm
u) Set (WQO Op)
ords)