{-# 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 forall a. MultiSet a -> Bool
MS.null MultiSet RuntimeTerm
trms
      then forall a. Show a => a -> String
show Op
op
      else forall a. Show a => a -> String
show Op
op forall a. [a] -> [a] -> [a]
++ 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 (forall a b. (a -> b) -> [a] -> [b]
map forall a. ToMetaTerm a => a -> MetaTerm
MT.toMetaTerm forall a b. (a -> b) -> a -> b
$ forall a. MultiSet a -> [a]
MS.toList MultiSet RuntimeTerm
xs)

type MultiSet = MS.MultiSet

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

rpoTerm :: RT.RuntimeTerm -> RuntimeTerm
rpoTerm :: RuntimeTerm -> RuntimeTerm
rpoTerm (RT.App Op
f [RuntimeTerm]
xs) = Op -> MultiSet RuntimeTerm -> RuntimeTerm
App Op
f forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> MultiSet a
MS.fromList (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 forall a. Eq a => a -> a -> Bool
== RuntimeTerm
u Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RuntimeTerm
t RuntimeTerm -> RuntimeTerm -> Bool
`isSubtermOf`) (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
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RPOState oc
st -> RPOState oc
st{rpoDepth :: Int
rpoDepth = forall (oc :: * -> *). RPOState oc -> Int
rpoDepth RPOState oc
st forall a. Num a => a -> a -> a
+ Int
1})
  oc Op
result <- RMonad oc (oc Op)
action
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RPOState oc
st -> RPOState oc
st{rpoDepth :: Int
rpoDepth = forall (oc :: * -> *). RPOState oc -> Int
rpoDepth RPOState oc
st forall a. Num a => a -> a -> a
- Int
1})
  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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall (oc :: * -> *). RPOState oc -> Cache oc
rpoCache
  case 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 -> 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
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\RPOState oc
st -> RPOState oc
st{ rpoCache :: Cache oc
rpoCache = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert CacheKey oc
key oc Op
result (forall (oc :: * -> *). RPOState oc -> Cache oc
rpoCache RPOState oc
st)})
      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 = forall (oc :: * -> *) base lifted a.
ConstraintGen oc base lifted (State a)
-> a -> ConstraintGen oc base lifted Identity
runStateConstraints (forall lifted' lifted (oc :: * -> *) base (m :: * -> *).
(lifted' -> lifted)
-> ConstraintGen oc base lifted m
-> ConstraintGen oc base lifted' m
cmapConstraints RuntimeTerm -> RuntimeTerm
rpoTerm forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm (RMonad oc)
rpo') (forall (oc :: * -> *). Cache oc -> Int -> RPOState oc
RPOState 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 = 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 forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm (RMonad oc)
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 forall a. Eq a => a -> a -> Bool
== forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable WQOConstraints oc m'
impl
rpo' OC{forall a. oc a
unsatisfiable :: forall a. oc a
unsatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable} Relation
r oc Op
oc      RuntimeTerm
t RuntimeTerm
u      | RuntimeTerm
t forall a. Eq a => a -> a -> Bool
== RuntimeTerm
u            = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Relation
r forall a. Eq a => a -> a -> Bool
== Relation
GT then forall a. oc a
unsatisfiable else oc Op
oc
rpo' OC{forall a. oc a
unsatisfiable :: forall a. oc a
unsatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable} Relation
_ oc Op
_       RuntimeTerm
t RuntimeTerm
u      | RuntimeTerm
t RuntimeTerm -> RuntimeTerm -> Bool
`isSubtermOf` RuntimeTerm
u = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. oc a
unsatisfiable
rpo' OC{forall a. oc a
unsatisfiable :: forall a. oc a
unsatisfiable :: forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m -> forall a. impl a
unsatisfiable} Relation
r oc Op
oc      RuntimeTerm
t RuntimeTerm
u      | RuntimeTerm
u RuntimeTerm -> RuntimeTerm -> Bool
`isSubtermOf` RuntimeTerm
t = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Relation
r forall a. Eq a => a -> a -> Bool
== Relation
EQ then 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 forall a. Eq a => a -> a -> Bool
== Op
g            = forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
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) = forall (oc :: * -> *). RMonad oc (oc Op) -> RMonad oc (oc Op)
incDepth StateT (RPOState oc) Identity (oc Op)
result
  where
    cs' :: oc Op
cs'    = 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 = 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) (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 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' = 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) forall a b. (a -> b) -> a -> b
$
      if Relation
r forall a. Eq a => a -> a -> Bool
== Relation
EQ
      then forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
rpoMul WQOConstraints oc m'
oc Relation
r (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 -> OpOrdering
=. Op
g) oc Op
cs') MultiSet RuntimeTerm
ts MultiSet RuntimeTerm
us
      else
        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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [
          forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
rpoMul WQOConstraints oc m'
oc Relation
GT  (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 -> OpOrdering
>. Op
g) oc Op
cs') (forall a. (Eq a, Hashable a) => a -> MultiSet a
MS.singleton RuntimeTerm
t) MultiSet RuntimeTerm
us
        , forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
rpoMul WQOConstraints oc m'
oc Relation
r   (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 -> OpOrdering
=. Op
g) oc Op
cs') MultiSet RuntimeTerm
ts               MultiSet RuntimeTerm
us
        , forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)
rpoMul WQOConstraints oc m'
oc Relation
GTE oc Op
cs'                             MultiSet RuntimeTerm
ts               (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 = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ 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
?impl (forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => impl a
noConstraints ?impl::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 = forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
rpo WQOConstraints oc m'
impl Relation
GTE


-- Non symbolic version

synEQ :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synEQ :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synEQ OpOrdering
o RuntimeTerm
l RuntimeTerm
r = OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' OpOrdering
o RuntimeTerm
l RuntimeTerm
r Bool -> Bool -> Bool
&& OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' OpOrdering
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 :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE OpOrdering
o RuntimeTerm
t RuntimeTerm
u = OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool
synGTE' OpOrdering
o (RuntimeTerm -> RuntimeTerm
rpoTerm RuntimeTerm
t) (RuntimeTerm -> RuntimeTerm
rpoTerm RuntimeTerm
u)

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

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

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

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