{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE FlexibleContexts #-}

-- | This module includes a typeclass for implementations of constraints on 'WQO's
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

-- | @WQOConstraints impl m@ defines an implementation for tracking and checking
--   satisfiability of constraints on arbitrary type @a@. Namely, instances of
--   @impl a@ are used to keep track of constraints. Satisfiability checking and
--   other computations are embedded in a computational context @m@.
data WQOConstraints impl m = OC
  {
    -- | @addConstraint wqo c@ adds constraints to @c@ to also permit the WQO @w@.
    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

    -- | @intersect c1 c2@ returns constraints to permit only WQOs permitted by both @c1@ and
    --   @c2@. Therefore the resulting constraints are stronger (less likely to be
    --   satisifiable).
  , 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
    -- | @isSatisfiable c@ returns true iff @c@ permits any WQO
  , 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

    -- | @c1 `notStrongerThan` c2@ iff any ordering permitted by @c1@ is also permitted
    --   by @c2@
  , 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
    -- | @noConstraints@ returns an instance of constraints that permits any WQO
  , 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
    -- | @c1 `union` c2@ returns constraints that permit WQOs permitted by /either/
    --  @c1@ or @c2@. The resulting constraints are therefore weaker (more likely to
    --  be satisfiable)
  , 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

    -- | @unsatisfiable@ returns an instance of constraints that does not permit any WQO
  , forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable       :: forall a. impl a

    -- | @getOrdering c@ returns a concrete ordering satisfying the constraints, if one exists
  , forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a -> Maybe (WQO a)
getOrdering         :: forall a. impl a -> Maybe (WQO a)
  }

-- | Returns true iff the constraints do not permit any WQO.
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

-- | Returns the constraints that permit a given WQO
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

-- | Given a list of constraints @ocs@, returns constraints that permit only the WQOs
--   permitted by each @oc@ in @ocs@
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

-- | Given a list of constraints @ocs@, returns constraints that permit the WQOs
--   permitted by any @oc@ in @ocs@
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 oc impl (f, g, r)@ strengthens constraints represented by @impl@
--   to also ensure that @f@ and @g@ are related via relation @r@ in permitted WQOs.
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)

-- | ConstraintGen impl R >= t u returns the constraints on >= that guarantee
-- the resulting relation >=', we have:
--   1. x >= y implies x >=' y
--   2. t lift(R(>=')) u
-- Where R generates { == , >=, > } from the underlying ordering
-- R is used to enable optimizations
type ConstraintGen oc base lifted m =
  forall m' . (WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base))

-- | @cmapConstraints@ takes a transformation @f@ from @lifted' to lifted@, and transforms
-- a constraint generator on terms of types @lifted@ into one on terms of types @lifted'@
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 f imp@ lifts the computations of @imp@ from context @m@ to context @m'@
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)

-- @runStateConstriants initState cgen@ transforms a constraint generator in the 'State'
-- monad to one in the 'Identity' monad by using initial state @initState@'
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