{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE FlexibleContexts #-}
module Language.REST.WQOConstraints
  (
    WQOConstraints(..)
  , ConstraintGen
  , liftC
  , cmapConstraints
  , numOrderings
  , 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 qualified Data.Set as S

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

trace' :: String -> a -> a
trace' :: String -> a -> a
trace' String
_ a
x = a
x

data WQOConstraints impl m = OC
  { 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
  , 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
  , 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
  , 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
  , WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints       :: forall a. (Eq a, Ord a, Hashable a) => impl a
  , 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
  , WQOConstraints impl m
-> forall a.
   (Eq a, Ord a, Hashable a) =>
   impl a -> Set a -> Set a -> impl a
relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a -> S.Set a -> impl a
  , 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
  , WQOConstraints impl m -> forall a. impl a
unsatisfiable       :: forall a. impl a
  , WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a -> Set a
elems               :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a
  , WQOConstraints impl m -> forall a. impl a -> Maybe (WQO a)
getOrdering         :: forall a. impl a -> Maybe (WQO a)
  , WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a
simplify            :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a
  }

numOrderings :: (Show a, Ord a, Eq a, Ord a, Hashable a) => S.Set a -> WQOConstraints oc m -> oc a -> Int
numOrderings :: Set a -> WQOConstraints oc m -> oc a -> Int
numOrderings Set a
elems WQOConstraints oc m
impl oc a
oc = Set (WQO a) -> Int
forall a. Set a -> Int
S.size (Set (WQO a) -> Int) -> Set (WQO a) -> Int
forall a b. (a -> b) -> a -> b
$ (WQO a -> Bool) -> Set (WQO a) -> Set (WQO a)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (WQOConstraints oc m -> oc a -> WQO a -> Bool
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   impl a -> WQO a -> Bool
permits WQOConstraints oc m
impl oc a
oc) (Set a -> Set (WQO a)
forall a. (Ord a, Eq a, Hashable a) => Set a -> Set (WQO a)
WQO.orderings Set a
elems)

isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool
isUnsatisfiable :: 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 (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> oc a -> m Bool
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 :: 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 = WQO a -> oc a -> oc a
forall a. (Eq a, Ord a, Hashable a) => WQO a -> oc a -> oc a
addConstraint WQO a
c oc a
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 :: 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} []     = oc a
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) = (oc a -> oc a -> oc a) -> oc a -> [oc a] -> oc a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' oc a -> oc a -> oc a
forall a.
(Show a, Show (oc a), Ord a, Hashable a) =>
oc a -> oc a -> oc a
go oc a
x [oc a]
xs
  where
    go :: oc a -> oc a -> oc a
go oc a
t1 oc a
t2 = String -> oc a -> oc a
forall a. String -> a -> a
trace' (String
"Intersect " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (oc a -> String
forall a. Show a => a -> String
show oc a
t1)) (oc a -> oc a) -> oc a -> oc a
forall a b. (a -> b) -> a -> b
$ oc a -> oc a -> oc a
forall a. (Show a, Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
intersect oc a
t1 oc a
t2

unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a
unionAll :: 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} []     = oc a
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) = (oc a -> oc a -> oc a) -> oc a -> [oc a] -> oc a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' oc a -> oc a -> oc a
forall a. (Show (oc a), Ord a, Hashable a) => oc a -> oc a -> oc a
go oc a
x [oc a]
xs
  where
    go :: oc a -> oc a -> oc a
go oc a
t1 oc a
t2 = String -> oc a -> oc a
forall a. String -> a -> a
trace' (String
"Union " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (oc a -> String
forall a. Show a => a -> String
show oc a
t1)) (oc a -> oc a) -> oc a -> oc a
forall a b. (a -> b) -> a -> b
$ oc a -> oc a -> oc a
forall a. (Eq a, Ord a, Hashable a) => oc a -> oc a -> oc a
union oc a
t1 oc a
t2

intersectRelation ::
  (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 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' -> WQOConstraints oc m -> oc a -> oc a -> oc a
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    -> WQOConstraints oc m -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m
oc
  where
    nc :: Relation -> Maybe (oc a)
nc Relation
GT  = (WQO a -> oc a) -> Maybe (WQO a) -> Maybe (oc a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (WQOConstraints oc m -> WQO a -> oc a
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc) ((a, a, QORelation) -> Maybe (WQO a)
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  = (WQO a -> oc a) -> Maybe (WQO a) -> Maybe (oc a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (WQOConstraints oc m -> WQO a -> oc a
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a) =>
WQOConstraints oc m -> WQO a -> oc a
singleton WQOConstraints oc m
oc) ((a, a, QORelation) -> Maybe (WQO a)
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 <- (a, a, QORelation) -> Maybe (WQO a)
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 <- (a, a, QORelation) -> Maybe (WQO a)
forall a.
(Ord a, Eq a, Hashable a) =>
(a, a, QORelation) -> Maybe (WQO a)
WQO.singleton (a
f, a
g, QORelation
WQO.QEQ)
      oc a -> Maybe (oc a)
forall (m :: * -> *) a. Monad m => a -> m a
return (oc a -> Maybe (oc a)) -> oc a -> Maybe (oc a)
forall a b. (a -> b) -> a -> b
$ WQOConstraints oc m -> oc a -> oc a -> oc a
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 (WQOConstraints oc m -> WQO a -> oc a
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) (WQOConstraints oc m -> WQO a -> oc a
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 :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m
cmapConstraints :: (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 = WQOConstraints oc m'
-> Relation -> oc base -> lifted -> lifted -> m (oc base)
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 :: (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, Eq a, Ord a, Hashable a) =>
impl a -> m' Bool
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, Eq a, Ord a, Hashable a) =>
impl a -> impl a -> m' Bool
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 (WQOConstraints impl m -> impl a -> m Bool
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 (WQOConstraints impl m -> impl 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 WQOConstraints impl m
oc impl a
c1 impl a
c2)

runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity
runStateConstraints :: 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 = oc base -> Identity (oc base)
forall a. a -> Identity a
Identity (oc base -> Identity (oc base)) -> oc base -> Identity (oc base)
forall a b. (a -> b) -> a -> b
$ State a (oc base) -> a -> oc base
forall s a. State s a -> s -> a
evalState (WQOConstraints oc m'
-> Relation -> oc base -> lifted -> lifted -> State a (oc base)
ConstraintGen oc base lifted (State a)
cgen WQOConstraints oc m'
impl Relation
r oc base
oc lifted
t lifted
u) a
initState