{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ImplicitParams #-}

-- | This module contains the implementation of the Recursive Path Quasi-Ordering,
--   defined in section 4.2.1 of the REST paper
module Language.REST.RPO (rpo, rpoGTE, synGTE) where

import Prelude hiding (EQ, GT)

import Control.Monad.Identity
import Control.Monad.State.Strict
import GHC.Generics
import Data.Hashable
import qualified Data.HashMap.Strict as M

import qualified Language.REST.Internal.MultiSet as MS
import           Language.REST.Op
import           Language.REST.Internal.OpOrdering as OpOrdering
import           Language.REST.WQOConstraints as OC
import qualified Language.REST.MetaTerm as MT
import           Language.REST.Types
import qualified Language.REST.RuntimeTerm as RT
import           Language.REST.Internal.MultisetOrder
import           Language.REST.Internal.Util

instance Show RuntimeTerm where
  show :: RuntimeTerm -> String
show (App Op
op MultiSet RuntimeTerm
trms) =
      if MultiSet RuntimeTerm -> Bool
forall a. MultiSet a -> Bool
MS.null MultiSet RuntimeTerm
trms
      then Op -> String
forall a. Show a => a -> String
show Op
op
      else Op -> String
forall a. Show a => a -> String
show Op
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ MultiSet RuntimeTerm -> String
forall a. Show a => a -> String
show MultiSet RuntimeTerm
trms

instance MT.ToMetaTerm RuntimeTerm where
  toMetaTerm :: RuntimeTerm -> MetaTerm
toMetaTerm (App Op
op MultiSet RuntimeTerm
xs) = Op -> [MetaTerm] -> MetaTerm
MT.RWApp Op
op ((RuntimeTerm -> MetaTerm) -> [RuntimeTerm] -> [MetaTerm]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> MetaTerm
forall a. ToMetaTerm a => a -> MetaTerm
MT.toMetaTerm ([RuntimeTerm] -> [MetaTerm]) -> [RuntimeTerm] -> [MetaTerm]
forall a b. (a -> b) -> a -> b
$ MultiSet RuntimeTerm -> [RuntimeTerm]
forall a. MultiSet a -> [a]
MS.toList MultiSet RuntimeTerm
xs)

type MultiSet = MS.MultiSet

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

rpoTerm :: RT.RuntimeTerm -> RuntimeTerm
rpoTerm :: RuntimeTerm -> RuntimeTerm
rpoTerm (RT.App Op
f [RuntimeTerm]
xs) = Op -> MultiSet RuntimeTerm -> RuntimeTerm
App Op
f (MultiSet RuntimeTerm -> RuntimeTerm)
-> MultiSet RuntimeTerm -> RuntimeTerm
forall a b. (a -> b) -> a -> b
$ [RuntimeTerm] -> MultiSet RuntimeTerm
forall a. (Eq a, Hashable a) => [a] -> MultiSet a
MS.fromList ((RuntimeTerm -> RuntimeTerm) -> [RuntimeTerm] -> [RuntimeTerm]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> RuntimeTerm
rpoTerm [RuntimeTerm]
xs)

isSubtermOf :: RuntimeTerm -> RuntimeTerm -> Bool
isSubtermOf :: RuntimeTerm -> RuntimeTerm -> Bool
isSubtermOf RuntimeTerm
t u :: RuntimeTerm
u@(App Op
_ MultiSet RuntimeTerm
us) = RuntimeTerm
t RuntimeTerm -> RuntimeTerm -> Bool
forall a. Eq a => a -> a -> Bool
== RuntimeTerm
u Bool -> Bool -> Bool
|| (RuntimeTerm -> Bool) -> [RuntimeTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RuntimeTerm
t RuntimeTerm -> RuntimeTerm -> Bool
`isSubtermOf`) (MultiSet RuntimeTerm -> [RuntimeTerm]
forall a. MultiSet a -> [a]
MS.distinctElems MultiSet RuntimeTerm
us)

type CacheKey oc = (oc Op, Relation, RuntimeTerm, RuntimeTerm)

type Cache oc = M.HashMap (CacheKey oc) (oc Op)

data RPOState oc =
  RPOState
    { forall (oc :: * -> *). RPOState oc -> Cache oc
rpoCache :: Cache oc
    , forall (oc :: * -> *). RPOState oc -> Int
rpoDepth :: Int
    }

type RMonad oc = State (RPOState oc)

incDepth :: RMonad oc (oc Op) -> RMonad oc (oc Op)
incDepth :: forall (oc :: * -> *). RMonad oc (oc Op) -> RMonad oc (oc Op)
incDepth RMonad oc (oc Op)
action = do
  (RPOState oc -> RPOState oc) -> StateT (RPOState oc) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RPOState oc
st -> RPOState oc
st{rpoDepth = rpoDepth st + 1})
  oc Op
result <- RMonad oc (oc Op)
action
  (RPOState oc -> RPOState oc) -> StateT (RPOState oc) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RPOState oc
st -> RPOState oc
st{rpoDepth = rpoDepth st - 1})
  oc Op -> RMonad oc (oc Op)
forall a. a -> StateT (RPOState oc) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return oc Op
result


cached :: (Eq (oc Op), Hashable (oc Op)) => CacheKey oc -> RMonad oc (oc Op) -> RMonad oc (oc Op)
cached :: forall (oc :: * -> *).
(Eq (oc Op), Hashable (oc Op)) =>
CacheKey oc -> RMonad oc (oc Op) -> RMonad oc (oc Op)
cached CacheKey oc
key RMonad oc (oc Op)
thunk = do
  Cache oc
cache <- (RPOState oc -> Cache oc)
-> StateT (RPOState oc) Identity (Cache oc)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets RPOState oc -> Cache oc
forall (oc :: * -> *). RPOState oc -> Cache oc
rpoCache
  case CacheKey oc -> Cache oc -> Maybe (oc Op)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup CacheKey oc
key Cache oc
cache of
    Just oc Op
result -> oc Op -> RMonad oc (oc Op)
forall a. a -> StateT (RPOState oc) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return oc Op
result
    Maybe (oc Op)
Nothing     -> do
      oc Op
result <- RMonad oc (oc Op)
thunk
      (RPOState oc -> RPOState oc) -> StateT (RPOState oc) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RPOState oc
st -> RPOState oc
st{ rpoCache = M.insert key result (rpoCache st)})
      oc Op -> RMonad oc (oc Op)
forall a. a -> StateT (RPOState oc) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return oc Op
result

-- | The constraint generator for RPQO. That is, given terms @t@, @u@, @rpo@ generates
--   the constraints on n RPQO ≥ᵣ such that t ≥ᵣ u.
rpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RT.RuntimeTerm Identity
rpo :: forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
rpo = ConstraintGen oc Op RuntimeTerm (State (RPOState oc))
-> RPOState oc -> ConstraintGen oc Op RuntimeTerm Identity
forall (oc :: * -> *) base lifted a.
ConstraintGen oc base lifted (State a)
-> a -> ConstraintGen oc base lifted Identity
runStateConstraints ((RuntimeTerm -> RuntimeTerm)
-> ConstraintGen oc Op RuntimeTerm (State (RPOState oc))
-> ConstraintGen oc Op RuntimeTerm (State (RPOState oc))
forall lifted' lifted (oc :: * -> *) base (m :: * -> *).
(lifted' -> lifted)
-> ConstraintGen oc base lifted m
-> ConstraintGen oc base lifted' m
cmapConstraints RuntimeTerm -> RuntimeTerm
rpoTerm WQOConstraints oc m'
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm (RMonad oc)
ConstraintGen oc Op RuntimeTerm (State (RPOState oc))
rpo') (Cache oc -> Int -> RPOState oc
forall (oc :: * -> *). Cache oc -> Int -> RPOState oc
RPOState Cache oc
forall k v. HashMap k v
M.empty Int
0)

rpoMul :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
rpoMul :: forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
rpoMul = ConstraintGen oc Op RuntimeTerm (StateT (RPOState oc) Identity)
-> ConstraintGen
     oc Op (MultiSet RuntimeTerm) (StateT (RPOState oc) Identity)
forall (oc :: * -> *) base lifted (m :: * -> *).
(Ord lifted, Ord base, Show base, Eq base, Hashable base,
 Hashable lifted, Eq lifted, Show (oc base), Eq (oc base),
 Monad m) =>
ConstraintGen oc base lifted m
-> ConstraintGen oc base (MultiSet lifted) m
multisetOrder WQOConstraints oc m'
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm (RMonad oc)
ConstraintGen oc Op RuntimeTerm (StateT (RPOState oc) Identity)
rpo'

rpo' :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm (RMonad oc)
rpo' :: forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm (RMonad oc)
rpo' WQOConstraints oc m'
impl Relation
_      oc Op
oc RuntimeTerm
_  RuntimeTerm
_ | oc Op
oc oc Op -> oc Op -> Bool
forall a. Eq a => a -> a -> Bool
== WQOConstraints oc m' -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl           = oc Op -> StateT (RPOState oc) Identity (oc Op)
forall a. a -> StateT (RPOState oc) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc Op -> StateT (RPOState oc) Identity (oc Op))
-> oc Op -> StateT (RPOState oc) Identity (oc Op)
forall a b. (a -> b) -> a -> b
$ WQOConstraints oc m' -> forall a. oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl
rpo' OC{forall a. oc a
unsatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable :: forall a. oc a
unsatisfiable} Relation
r oc Op
oc      RuntimeTerm
t RuntimeTerm
u      | RuntimeTerm
t RuntimeTerm -> RuntimeTerm -> Bool
forall a. Eq a => a -> a -> Bool
== RuntimeTerm
u            = oc Op -> StateT (RPOState oc) Identity (oc Op)
forall a. a -> StateT (RPOState oc) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc Op -> StateT (RPOState oc) Identity (oc Op))
-> oc Op -> StateT (RPOState oc) Identity (oc Op)
forall a b. (a -> b) -> a -> b
$ if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
GT then oc Op
forall a. oc a
unsatisfiable else oc Op
oc
rpo' OC{forall a. oc a
unsatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable :: forall a. oc a
unsatisfiable} Relation
_ oc Op
_       RuntimeTerm
t RuntimeTerm
u      | RuntimeTerm
t RuntimeTerm -> RuntimeTerm -> Bool
`isSubtermOf` RuntimeTerm
u = oc Op -> StateT (RPOState oc) Identity (oc Op)
forall a. a -> StateT (RPOState oc) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return oc Op
forall a. oc a
unsatisfiable
rpo' OC{forall a. oc a
unsatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable :: forall a. oc a
unsatisfiable} Relation
r oc Op
oc      RuntimeTerm
t RuntimeTerm
u      | RuntimeTerm
u RuntimeTerm -> RuntimeTerm -> Bool
`isSubtermOf` RuntimeTerm
t = oc Op -> StateT (RPOState oc) Identity (oc Op)
forall a. a -> StateT (RPOState oc) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (oc Op -> StateT (RPOState oc) Identity (oc Op))
-> oc Op -> StateT (RPOState oc) Identity (oc Op)
forall a b. (a -> b) -> a -> b
$ if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
EQ then oc Op
forall a. oc a
unsatisfiable else oc Op
oc
rpo' WQOConstraints oc m'
oc Relation
r oc Op
cs (App Op
f MultiSet RuntimeTerm
ts) (App Op
g MultiSet RuntimeTerm
us)        | Op
f Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
g            = WQOConstraints oc m'
-> Relation
-> oc Op
-> MultiSet RuntimeTerm
-> MultiSet RuntimeTerm
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
ConstraintGen
  oc Op (MultiSet RuntimeTerm) (StateT (RPOState oc) Identity)
rpoMul WQOConstraints oc m'
oc Relation
r oc Op
cs MultiSet RuntimeTerm
ts MultiSet RuntimeTerm
us

rpo' WQOConstraints oc m'
oc Relation
r oc Op
cs t :: RuntimeTerm
t@(App Op
f MultiSet RuntimeTerm
ts) u :: RuntimeTerm
u@(App Op
g MultiSet RuntimeTerm
us) = StateT (RPOState oc) Identity (oc Op)
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *). RMonad oc (oc Op) -> RMonad oc (oc Op)
incDepth StateT (RPOState oc) Identity (oc Op)
result
  where
    cs' :: oc Op
cs'    = WQOConstraints oc m' -> forall a. (Eq a, Ord a, Hashable a) => oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints WQOConstraints oc m'
oc
    result :: StateT (RPOState oc) Identity (oc Op)
result = CacheKey oc
-> StateT (RPOState oc) Identity (oc Op)
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Eq (oc Op), Hashable (oc Op)) =>
CacheKey oc -> RMonad oc (oc Op) -> RMonad oc (oc Op)
cached (oc Op
cs, Relation
r, RuntimeTerm
t, RuntimeTerm
u) (WQOConstraints oc m'
-> forall a.
   (Show a, Eq a, Ord a, Hashable a) =>
   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 Op
cs (oc Op -> oc Op)
-> StateT (RPOState oc) Identity (oc Op)
-> StateT (RPOState oc) Identity (oc Op)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (RPOState oc) Identity (oc Op)
result')
    result' :: StateT (RPOState oc) Identity (oc Op)
result' = CacheKey oc
-> StateT (RPOState oc) Identity (oc Op)
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Eq (oc Op), Hashable (oc Op)) =>
CacheKey oc -> RMonad oc (oc Op) -> RMonad oc (oc Op)
cached (oc Op
cs', Relation
r, RuntimeTerm
t, RuntimeTerm
u) (StateT (RPOState oc) Identity (oc Op)
 -> StateT (RPOState oc) Identity (oc Op))
-> StateT (RPOState oc) Identity (oc Op)
-> StateT (RPOState oc) Identity (oc Op)
forall a b. (a -> b) -> a -> b
$
      if Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
EQ
      then WQOConstraints oc m'
-> Relation
-> oc Op
-> MultiSet RuntimeTerm
-> MultiSet RuntimeTerm
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
ConstraintGen
  oc Op (MultiSet RuntimeTerm) (StateT (RPOState oc) Identity)
rpoMul WQOConstraints oc m'
oc Relation
r (WQOConstraints oc m'
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> oc a -> oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
addConstraint WQOConstraints oc m'
oc (Op
f Op -> Op -> WQO Op
=. Op
g) oc Op
cs') MultiSet RuntimeTerm
ts MultiSet RuntimeTerm
us
      else
        WQOConstraints oc m' -> [oc Op] -> oc Op
forall a (oc :: * -> *) (m :: * -> *).
(Eq a, Ord a, Hashable a, Show a, Show (oc a)) =>
WQOConstraints oc m -> [oc a] -> oc a
unionAll WQOConstraints oc m'
oc ([oc Op] -> oc Op)
-> StateT (RPOState oc) Identity [oc Op]
-> StateT (RPOState oc) Identity (oc Op)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [StateT (RPOState oc) Identity (oc Op)]
-> StateT (RPOState oc) Identity [oc Op]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [
          WQOConstraints oc m'
-> Relation
-> oc Op
-> MultiSet RuntimeTerm
-> MultiSet RuntimeTerm
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
ConstraintGen
  oc Op (MultiSet RuntimeTerm) (StateT (RPOState oc) Identity)
rpoMul WQOConstraints oc m'
oc Relation
GT  (WQOConstraints oc m'
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> oc a -> oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
addConstraint WQOConstraints oc m'
oc (Op
f Op -> Op -> WQO Op
>. Op
g) oc Op
cs') (RuntimeTerm -> MultiSet RuntimeTerm
forall a. (Eq a, Hashable a) => a -> MultiSet a
MS.singleton RuntimeTerm
t) MultiSet RuntimeTerm
us
        , WQOConstraints oc m'
-> Relation
-> oc Op
-> MultiSet RuntimeTerm
-> MultiSet RuntimeTerm
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
ConstraintGen
  oc Op (MultiSet RuntimeTerm) (StateT (RPOState oc) Identity)
rpoMul WQOConstraints oc m'
oc Relation
r   (WQOConstraints oc m'
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> oc a -> oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
addConstraint WQOConstraints oc m'
oc (Op
f Op -> Op -> WQO Op
=. Op
g) oc Op
cs') MultiSet RuntimeTerm
ts               MultiSet RuntimeTerm
us
        , WQOConstraints oc m'
-> Relation
-> oc Op
-> MultiSet RuntimeTerm
-> MultiSet RuntimeTerm
-> StateT (RPOState oc) Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
ConstraintGen
  oc Op (MultiSet RuntimeTerm) (StateT (RPOState oc) Identity)
rpoMul WQOConstraints oc m'
oc Relation
GTE oc Op
cs'                             MultiSet RuntimeTerm
ts               (RuntimeTerm -> MultiSet RuntimeTerm
forall a. (Eq a, Hashable a) => a -> MultiSet a
MS.singleton RuntimeTerm
u)
        ]

-- | @rpoGTE impl t u@ generates the constraints a WQO over 'Op' (via @impl@) that ensures
--   that t ≥ᵣ u in the result RPQO ≥ᵣ.
rpoGTE
  :: (?impl::WQOConstraints oc m, Hashable (oc Op), Eq (oc Op), Show (oc Op))
  => RT.RuntimeTerm
  -> RT.RuntimeTerm
  -> oc Op
rpoGTE :: forall (oc :: * -> *) (m :: * -> *).
(?impl::WQOConstraints oc m, Hashable (oc Op), Eq (oc Op),
 Show (oc Op)) =>
RuntimeTerm -> RuntimeTerm -> oc Op
rpoGTE RuntimeTerm
t RuntimeTerm
u = Identity (oc Op) -> oc Op
forall a. Identity a -> a
runIdentity (Identity (oc Op) -> oc Op) -> Identity (oc Op) -> oc Op
forall a b. (a -> b) -> a -> b
$ WQOConstraints oc m
-> oc Op -> RuntimeTerm -> RuntimeTerm -> Identity (oc Op)
forall (oc :: * -> *) (m' :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
WQOConstraints oc m'
-> oc Op -> RuntimeTerm -> RuntimeTerm -> Identity (oc Op)
rpoGTE' ?impl::WQOConstraints oc m
WQOConstraints oc m
?impl (WQOConstraints oc m -> forall a. (Eq a, Ord a, Hashable a) => oc a
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints ?impl::WQOConstraints oc m
WQOConstraints oc m
?impl) RuntimeTerm
t RuntimeTerm
u

rpoGTE'
  :: (Show (oc Op), Eq (oc Op), Hashable (oc Op))
  => WQOConstraints oc m'
  -> oc Op
  -> RT.RuntimeTerm
  -> RT.RuntimeTerm
  -> Identity (oc Op)
rpoGTE' :: forall (oc :: * -> *) (m' :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
WQOConstraints oc m'
-> oc Op -> RuntimeTerm -> RuntimeTerm -> Identity (oc Op)
rpoGTE' WQOConstraints oc m'
impl = WQOConstraints oc m'
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
ConstraintGen oc Op RuntimeTerm Identity
rpo WQOConstraints oc m'
impl Relation
GTE


-- Non symbolic version

synEQ :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synEQ :: WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synEQ WQO Op
o RuntimeTerm
l RuntimeTerm
r = WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' WQO Op
o RuntimeTerm
l RuntimeTerm
r Bool -> Bool -> Bool
&& WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' WQO Op
o RuntimeTerm
r RuntimeTerm
l

-- | Performs the (concrete) RPQO calculation. @synGTE o t u@ returns
--   true iff t ≥ᵣ u using an RPQO with precedence @o@.
synGTE :: OpOrdering -> RT.RuntimeTerm -> RT.RuntimeTerm -> Bool
synGTE :: WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE WQO Op
o RuntimeTerm
t RuntimeTerm
u = WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' WQO Op
o (RuntimeTerm -> RuntimeTerm
rpoTerm RuntimeTerm
t) (RuntimeTerm -> RuntimeTerm
rpoTerm RuntimeTerm
u)

synGTE' :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' :: WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' WQO Op
ordering t :: RuntimeTerm
t@(App Op
f MultiSet RuntimeTerm
_ts) (App Op
g MultiSet RuntimeTerm
us)
  | WQO Op -> Op -> Op -> Bool
opGT WQO Op
ordering Op
f Op
g
  = WQO Op -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool
synGTM WQO Op
ordering (RuntimeTerm -> MultiSet RuntimeTerm
forall a. (Eq a, Hashable a) => a -> MultiSet a
MS.singleton RuntimeTerm
t) MultiSet RuntimeTerm
us
synGTE' WQO Op
ordering (App Op
f MultiSet RuntimeTerm
ts) (App Op
g MultiSet RuntimeTerm
us)
  | WQO Op -> Op -> Op -> Bool
opEQ WQO Op
ordering Op
f Op
g
  = WQO Op -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool
synGTEM WQO Op
ordering MultiSet RuntimeTerm
ts MultiSet RuntimeTerm
us
synGTE' WQO Op
ordering (App Op
_ MultiSet RuntimeTerm
ts) RuntimeTerm
u = WQO Op -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool
synGTEM WQO Op
ordering MultiSet RuntimeTerm
ts (RuntimeTerm -> MultiSet RuntimeTerm
forall a. (Eq a, Hashable a) => a -> MultiSet a
MS.singleton RuntimeTerm
u)

rpoT :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
rpoT :: WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
rpoT WQO Op
o RuntimeTerm
t1 RuntimeTerm
t2 = WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' WQO Op
o RuntimeTerm
t1 RuntimeTerm
t2 Bool -> Bool -> Bool
&& Bool -> Bool
not (WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' WQO Op
o RuntimeTerm
t2 RuntimeTerm
t1)

synGTEM :: OpOrdering -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool
synGTEM :: WQO Op -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool
synGTEM WQO Op
ordering MultiSet RuntimeTerm
xs MultiSet RuntimeTerm
ys = case (RuntimeTerm -> RuntimeTerm -> Bool)
-> [RuntimeTerm] -> [RuntimeTerm] -> ([RuntimeTerm], [RuntimeTerm])
forall a. Eq a => (a -> a -> Bool) -> [a] -> [a] -> ([a], [a])
removeEqBy (WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synEQ WQO Op
ordering) (MultiSet RuntimeTerm -> [RuntimeTerm]
forall a. MultiSet a -> [a]
MS.toList MultiSet RuntimeTerm
xs) (MultiSet RuntimeTerm -> [RuntimeTerm]
forall a. MultiSet a -> [a]
MS.toList MultiSet RuntimeTerm
ys) of
  ([RuntimeTerm]
xs', [RuntimeTerm]
ys') -> (RuntimeTerm -> Bool) -> [RuntimeTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\RuntimeTerm
y -> (RuntimeTerm -> Bool) -> [RuntimeTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\RuntimeTerm
x -> WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
rpoT WQO Op
ordering RuntimeTerm
x RuntimeTerm
y) [RuntimeTerm]
xs') [RuntimeTerm]
ys'

synGTM :: OpOrdering -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool
synGTM :: WQO Op -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool
synGTM WQO Op
ordering MultiSet RuntimeTerm
xs MultiSet RuntimeTerm
ys = case (RuntimeTerm -> RuntimeTerm -> Bool)
-> [RuntimeTerm] -> [RuntimeTerm] -> ([RuntimeTerm], [RuntimeTerm])
forall a. Eq a => (a -> a -> Bool) -> [a] -> [a] -> ([a], [a])
removeEqBy (WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
synEQ WQO Op
ordering) (MultiSet RuntimeTerm -> [RuntimeTerm]
forall a. MultiSet a -> [a]
MS.toList MultiSet RuntimeTerm
xs) (MultiSet RuntimeTerm -> [RuntimeTerm]
forall a. MultiSet a -> [a]
MS.toList MultiSet RuntimeTerm
ys) of
  ([] , [] ) -> Bool
False
  ([RuntimeTerm]
xs', [RuntimeTerm]
ys') -> (RuntimeTerm -> Bool) -> [RuntimeTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\RuntimeTerm
y -> (RuntimeTerm -> Bool) -> [RuntimeTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\RuntimeTerm
x -> WQO Op -> RuntimeTerm -> RuntimeTerm -> Bool
rpoT WQO Op
ordering RuntimeTerm
x RuntimeTerm
y) [RuntimeTerm]
xs') [RuntimeTerm]
ys'