{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE FlexibleContexts #-}
module Language.REST.WQOConstraints
(
WQOConstraints(..)
, ConstraintGen
, liftC
, cmapConstraints
, isUnsatisfiable
, intersectAll
, unionAll
, intersectRelation
, runStateConstraints
, singleton
) where
import Control.Monad.Identity
import Control.Monad.State.Strict
import qualified Data.List as L
import Data.Hashable
import Prelude hiding (GT, EQ)
import qualified Language.REST.Internal.WQO as WQO
import Language.REST.Types
import Language.REST.SMT (ToSMTVar)
type WQO = WQO.WQO
data WQOConstraints impl m = OC
{
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
addConstraint :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a
intersect :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
impl a -> m Bool
isSatisfiable :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> m Bool
notStrongerThan :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> WQO a -> Bool
permits :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> WQO a -> Bool
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a
union :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable :: forall a. impl a
, forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a -> Maybe (WQO a)
getOrdering :: forall a. impl a -> Maybe (WQO a)
}
isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool
isUnsatisfiable :: forall (m :: * -> *) a (oc :: * -> *).
(Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> oc a -> m Bool
isUnsatisfiable OC{forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
oc a -> m Bool
isSatisfiable :: forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
oc a -> m Bool
isSatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
impl a -> m Bool
isSatisfiable} oc a
c = Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
oc a -> m Bool
isSatisfiable oc a
c
singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a
singleton :: forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton OC{forall a. (Eq a, Ord a, Hashable a) => WQO a -> oc a -> oc a
addConstraint :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> oc a -> oc a
addConstraint :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
addConstraint, forall a. (Eq a, Ord a, Hashable a) => oc a
noConstraints :: forall a. (Eq a, Ord a, Hashable a) => oc a
noConstraints :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints} WQO a
c = forall a. (Eq a, Ord a, Hashable a) => WQO a -> oc a -> oc a
addConstraint WQO a
c forall a. (Eq a, Ord a, Hashable a) => oc a
noConstraints
intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a
intersectAll :: forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
intersectAll OC{forall a. (Eq a, Ord a, Hashable a) => oc a
noConstraints :: forall a. (Eq a, Ord a, Hashable a) => oc a
noConstraints :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints} [] = forall a. (Eq a, Ord a, Hashable a) => oc a
noConstraints
intersectAll OC{forall a. (Show a, Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
intersect :: forall a. (Show a, Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
intersect :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a
intersect} (oc a
x:[oc a]
xs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' forall a. (Show a, Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
intersect oc a
x [oc a]
xs
unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a
unionAll :: forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
unionAll OC{forall a. oc a
unsatisfiable :: forall a. oc a
unsatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable} [] = forall a. oc a
unsatisfiable
unionAll OC{forall a. (Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
union :: forall a. (Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
union :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a
union} (oc a
x:[oc a]
xs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' forall a. (Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
union oc a
x [oc a]
xs
intersectRelation ::
(Ord a, Eq a, Ord a, Hashable a, Show a) =>
WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a
intersectRelation :: forall a (oc :: * -> *) (m :: * -> *).
(Ord a, Eq a, Ord a, Hashable a, Show a) =>
WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a
intersectRelation WQOConstraints oc m
oc oc a
impl (a
f, a
g, Relation
r) =
case Relation -> Maybe (oc a)
nc Relation
r of
Just oc a
impl' -> forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(Show a, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a
intersect WQOConstraints oc m
oc oc a
impl oc a
impl'
Maybe (oc a)
Nothing -> forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
where
nc :: Relation -> Maybe (oc a)
nc Relation
GT = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc) (forall a.
(Ord a, Eq a, Hashable a) =>
(a, a, QORelation) -> Maybe (WQO a)
WQO.singleton (a
f, a
g, QORelation
WQO.QGT))
nc Relation
EQ = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc) (forall a.
(Ord a, Eq a, Hashable a) =>
(a, a, QORelation) -> Maybe (WQO a)
WQO.singleton (a
f, a
g, QORelation
WQO.QEQ))
nc Relation
GTE = do
WQO a
wqo1 <- forall a.
(Ord a, Eq a, Hashable a) =>
(a, a, QORelation) -> Maybe (WQO a)
WQO.singleton (a
f, a
g, QORelation
WQO.QGT)
WQO a
wqo2 <- forall a.
(Ord a, Eq a, Hashable a) =>
(a, a, QORelation) -> Maybe (WQO a)
WQO.singleton (a
f, a
g, QORelation
WQO.QEQ)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(Eq a, Ord a, Hashable a) =>
impl a -> impl a -> impl a
union WQOConstraints oc m
oc (forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc WQO a
wqo1) (forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc WQO a
wqo2)
type ConstraintGen oc base lifted m =
forall m' . (WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base))
cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m
cmapConstraints :: forall lifted' lifted (oc :: * -> *) base (m :: * -> *).
(lifted' -> lifted)
-> ConstraintGen oc base lifted m
-> ConstraintGen oc base lifted' m
cmapConstraints lifted' -> lifted
f ConstraintGen oc base lifted m
cgen WQOConstraints oc m'
impl Relation
r oc base
oc lifted'
t lifted'
u = ConstraintGen oc base lifted m
cgen WQOConstraints oc m'
impl Relation
r oc base
oc (lifted' -> lifted
f lifted'
t) (lifted' -> lifted
f lifted'
u)
liftC :: (m Bool -> m' Bool) -> WQOConstraints impl m -> WQOConstraints impl m'
liftC :: forall (m :: * -> *) (m' :: * -> *) (impl :: * -> *).
(m Bool -> m' Bool)
-> WQOConstraints impl m -> WQOConstraints impl m'
liftC m Bool -> m' Bool
f WQOConstraints impl m
oc = WQOConstraints impl m
oc{
isSatisfiable :: forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
impl a -> m' Bool
isSatisfiable = forall {a}.
(ToSMTVar a Int, Show a, Ord a, Hashable a) =>
impl a -> m' Bool
isSatisfiable'
, notStrongerThan :: forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> m' Bool
notStrongerThan = forall {a}.
(ToSMTVar a Int, Ord a, Hashable a) =>
impl a -> impl a -> m' Bool
notStrongerThan'
}
where
isSatisfiable' :: impl a -> m' Bool
isSatisfiable' impl a
c1 = m Bool -> m' Bool
f (forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
impl a -> m Bool
isSatisfiable WQOConstraints impl m
oc impl a
c1)
notStrongerThan' :: impl a -> impl a -> m' Bool
notStrongerThan' impl a
c1 impl a
c2 = m Bool -> m' Bool
f (forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> m Bool
notStrongerThan WQOConstraints impl m
oc impl a
c1 impl a
c2)
runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity
runStateConstraints :: forall (oc :: * -> *) base lifted a.
ConstraintGen oc base lifted (State a)
-> a -> ConstraintGen oc base lifted Identity
runStateConstraints ConstraintGen oc base lifted (State a)
cgen a
initState WQOConstraints oc m'
impl Relation
r oc base
oc lifted
t lifted
u = forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> a
evalState (ConstraintGen oc base lifted (State a)
cgen WQOConstraints oc m'
impl Relation
r oc base
oc lifted
t lifted
u) a
initState