{-# 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 forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: ConcreteOC -> ConcreteOC -> Bool $c/= :: ConcreteOC -> ConcreteOC -> Bool == :: ConcreteOC -> ConcreteOC -> Bool $c== :: ConcreteOC -> ConcreteOC -> Bool Eq, Eq 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 min :: ConcreteOC -> ConcreteOC -> ConcreteOC $cmin :: ConcreteOC -> ConcreteOC -> ConcreteOC max :: ConcreteOC -> ConcreteOC -> ConcreteOC $cmax :: ConcreteOC -> ConcreteOC -> ConcreteOC >= :: ConcreteOC -> ConcreteOC -> Bool $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 compare :: ConcreteOC -> ConcreteOC -> Ordering $ccompare :: ConcreteOC -> ConcreteOC -> Ordering Ord, 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 $cto :: forall x. Rep ConcreteOC x -> ConcreteOC $cfrom :: forall x. ConcreteOC -> Rep ConcreteOC x Generic, Eq ConcreteOC Int -> ConcreteOC -> Int ConcreteOC -> Int forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a hash :: ConcreteOC -> Int $chash :: ConcreteOC -> Int hashWithSalt :: Int -> ConcreteOC -> Int $chashWithSalt :: Int -> ConcreteOC -> Int Hashable) instance Show ConcreteOC where show :: ConcreteOC -> String show (ConcreteOC Set (WQO Op) ords) = forall a. Show a => a -> String show (forall a. Set a -> Int S.size Set (WQO Op) ords) 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 = 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 (forall (m :: * -> *) a. Monad m => a -> m a return forall b c a. (b -> c) -> (a -> b) -> a -> c . ConcreteOC -> Bool isSat) ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC refine (Set (WQO Op) -> ConcreteOC ConcreteOC (forall a. (Ord a, Eq a, Hashable a) => Set a -> Set (WQO a) WQO.orderings Set Op ops)) ConcreteOC -> ConcreteOC -> ConcreteOC union 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 forall a b. (a -> b) -> a -> b $ 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) = forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Set (WQO Op) ord1 forall a. Eq a => a -> a -> Bool == Set (WQO Op) ord2 Bool -> Bool -> Bool || Set (WQO Op) ord2 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 forall a b. (a -> b) -> a -> b $ 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 (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)