{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# OPTIONS_GHC -Wno-error=deprecations #-}
module Language.REST.Rest (
rest
, pathsResult
, termsResult
, PathsResult(..)
, TermsResult
, WorkStrategy(..)
, RESTParams(..)
, RESTResult(..)
) where
import Control.Monad
import Control.Monad.Trans
import Data.Hashable
import qualified Data.HashSet as S
import qualified Data.List as L
import qualified Data.HashMap.Strict as M
import qualified Data.Maybe as Mb
import Language.REST.OCAlgebra as AC
import Language.REST.RewriteRule
import Language.REST.Path
import Language.REST.ExploredTerms as ET
import Language.REST.Internal.ListT
import Language.REST.Internal.WorkStrategy
newtype PathsResult rule term oc = PathsResult (S.HashSet (Path rule term oc))
newtype TermsResult rule term oc = TermsResult (S.HashSet term)
pathsResult :: PathsResult rule term oc
pathsResult :: forall rule term oc. PathsResult rule term oc
pathsResult = forall rule term oc.
HashSet (Path rule term oc) -> PathsResult rule term oc
PathsResult forall a. HashSet a
S.empty
termsResult :: TermsResult rule term oc
termsResult :: forall rule term oc. TermsResult rule term oc
termsResult = forall rule term oc. HashSet term -> TermsResult rule term oc
TermsResult forall a. HashSet a
S.empty
class RESTResult a where
includeInResult :: (Hashable oc, Eq oc, Hashable rule, Eq rule, Hashable term, Eq term) => Path rule term oc -> a rule term oc -> a rule term oc
resultTerms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term
instance RESTResult PathsResult where
includeInResult :: forall oc rule term.
(Hashable oc, Eq oc, Hashable rule, Eq rule, Hashable term,
Eq term) =>
Path rule term oc
-> PathsResult rule term oc -> PathsResult rule term oc
includeInResult Path rule term oc
p (PathsResult HashSet (Path rule term oc)
s) = forall rule term oc.
HashSet (Path rule term oc) -> PathsResult rule term oc
PathsResult (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Path rule term oc
p HashSet (Path rule term oc)
s)
resultTerms :: forall term rule oc.
(Eq term, Hashable term) =>
PathsResult rule term oc -> HashSet term
resultTerms (PathsResult HashSet (Path rule term oc)
s) = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall rule term a. Path rule term a -> [term]
pathTerms forall a b. (a -> b) -> a -> b
$ forall a. HashSet a -> [a]
S.toList HashSet (Path rule term oc)
s)
instance RESTResult TermsResult where
includeInResult :: forall oc rule term.
(Hashable oc, Eq oc, Hashable rule, Eq rule, Hashable term,
Eq term) =>
Path rule term oc
-> TermsResult rule term oc -> TermsResult rule term oc
includeInResult Path rule term oc
p (TermsResult HashSet term
s) = forall rule term oc. HashSet term -> TermsResult rule term oc
TermsResult (forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet term
s (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall rule term a. Path rule term a -> [term]
pathTerms Path rule term oc
p))
resultTerms :: forall term rule oc.
(Eq term, Hashable term) =>
TermsResult rule term oc -> HashSet term
resultTerms (TermsResult HashSet term
s) = HashSet term
s
data RESTState m rule term oc et rtype = RESTState
{ forall (m :: * -> *) rule term oc et (rtype :: * -> * -> * -> *).
RESTState m rule term oc et rtype -> rtype rule term oc
finished :: rtype rule term oc
, forall (m :: * -> *) rule term oc et (rtype :: * -> * -> * -> *).
RESTState m rule term oc et rtype -> [Path rule term oc]
working :: [Path rule term oc]
, forall (m :: * -> *) rule term oc et (rtype :: * -> * -> * -> *).
RESTState m rule term oc et rtype -> ExploredTerms term oc m
explored :: ExploredTerms term oc m
, forall (m :: * -> *) rule term oc et (rtype :: * -> * -> * -> *).
RESTState m rule term oc et rtype -> Maybe (Path rule term oc)
targetPath :: Maybe (Path rule term oc)
}
data RESTParams m rule term oc rtype = RESTParams
{ forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> HashSet rule
re :: S.HashSet rule
, forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> HashSet rule
ru :: S.HashSet rule
, forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> Maybe term
target :: Maybe term
, forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> WorkStrategy rule term oc
workStrategy :: WorkStrategy rule term oc
, forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> OCAlgebra oc term m
ocImpl :: OCAlgebra oc term m
, forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> rtype rule term oc
initRes :: rtype rule term oc
, forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> ExploreStrategy
etStrategy :: ExploreStrategy
}
rest :: forall m rule term oc rtype .
( MonadIO m
, RewriteRule m rule term
, Hashable term
, Eq term
, Hashable rule
, Hashable oc
, Eq rule
, Eq oc
, Show oc
, RESTResult rtype)
=> RESTParams m rule term oc rtype
-> term
-> m (rtype rule term oc, Maybe (Path rule term oc))
rest :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
(MonadIO m, RewriteRule m rule term, Hashable term, Eq term,
Hashable rule, Hashable oc, Eq rule, Eq oc, Show oc,
RESTResult rtype) =>
RESTParams m rule term oc rtype
-> term -> m (rtype rule term oc, Maybe (Path rule term oc))
rest RESTParams{HashSet rule
re :: HashSet rule
re :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> HashSet rule
re,HashSet rule
ru :: HashSet rule
ru :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> HashSet rule
ru,OCAlgebra oc term m
ocImpl :: OCAlgebra oc term m
ocImpl :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> OCAlgebra oc term m
ocImpl,WorkStrategy rule term oc
workStrategy :: WorkStrategy rule term oc
workStrategy :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> WorkStrategy rule term oc
workStrategy,rtype rule term oc
initRes :: rtype rule term oc
initRes :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> rtype rule term oc
initRes,Maybe term
target :: Maybe term
target :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> Maybe term
target,ExploreStrategy
etStrategy :: ExploreStrategy
etStrategy :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> ExploreStrategy
etStrategy} term
t =
forall {rtype :: * -> * -> * -> *} {et}.
RESTResult rtype =>
RESTState m rule term oc et rtype
-> m (rtype rule term oc, Maybe (Path rule term oc))
rest' (forall (m :: * -> *) rule term oc et (rtype :: * -> * -> * -> *).
rtype rule term oc
-> [Path rule term oc]
-> ExploredTerms term oc m
-> Maybe (Path rule term oc)
-> RESTState m rule term oc et rtype
RESTState rtype rule term oc
initRes [([], forall rule term.
term -> HashSet (term, rule) -> PathTerm rule term
PathTerm term
t forall a. HashSet a
S.empty)] ExploredTerms term oc m
initET forall a. Maybe a
Nothing)
where
(WorkStrategy forall (m :: * -> *). GetWork m rule term oc
ws) = WorkStrategy rule term oc
workStrategy
initET :: ExploredTerms term oc m
initET = forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ET.empty (forall term c (m :: * -> *).
(c -> c -> c)
-> (c -> c -> m Bool)
-> (c -> term -> term -> c)
-> ExploreFuncs term c m
EF (forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
AC.union OCAlgebra oc term m
ocImpl) (forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
AC.notStrongerThan OCAlgebra oc term m
ocImpl) (forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra oc term m
ocImpl)) ExploreStrategy
etStrategy
rest' :: RESTState m rule term oc et rtype
-> m (rtype rule term oc, Maybe (Path rule term oc))
rest' (RESTState rtype rule term oc
fin [] ExploredTerms term oc m
_ Maybe (Path rule term oc)
targetPath) = forall (m :: * -> *) a. Monad m => a -> m a
return (rtype rule term oc
fin, Maybe (Path rule term oc)
targetPath)
rest' state :: RESTState m rule term oc et rtype
state@(RESTState rtype rule term oc
_ [Path rule term oc]
paths ExploredTerms term oc m
et (Just Path rule term oc
targetPath))
| (([Step rule term oc]
steps, PathTerm rule term
_), [Path rule term oc]
remaining) <- forall (m :: * -> *). GetWork m rule term oc
ws [Path rule term oc]
paths ExploredTerms term oc m
et
, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step rule term oc]
steps forall a. Ord a => a -> a -> Bool
>= forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a b. (a, b) -> a
fst Path rule term oc
targetPath)
= RESTState m rule term oc et rtype
-> m (rtype rule term oc, Maybe (Path rule term oc))
rest' RESTState m rule term oc et rtype
state{working :: [Path rule term oc]
working = [Path rule term oc]
remaining}
rest' state :: RESTState m rule term oc et rtype
state@(RESTState rtype rule term oc
fin [Path rule term oc]
paths ExploredTerms term oc m
et Maybe (Path rule term oc)
targetPath) = do
Bool
se <- forall term c (m :: * -> *).
(Monad m, Eq term, Hashable term, Eq c, Show c, Hashable c) =>
term -> c -> ExploredTerms term c m -> m Bool
shouldExplore term
ptTerm oc
lastOrdering ExploredTerms term oc m
et
if Bool
se
then do
HashSet (term, rule)
evalRWs <- HashSet rule -> m (HashSet (term, rule))
candidates HashSet rule
re
HashSet (term, rule)
userRWs <- HashSet rule -> m (HashSet (term, rule))
candidates HashSet rule
ru
HashMap term oc
acceptedUserRWs <- HashSet (term, rule) -> m (HashMap term oc)
accepted HashSet (term, rule)
userRWs
HashSet (term, rule)
-> HashSet (term, rule)
-> HashMap term oc
-> m (rtype rule term oc, Maybe (Path rule term oc))
go HashSet (term, rule)
evalRWs HashSet (term, rule)
userRWs HashMap term oc
acceptedUserRWs
else
RESTState m rule term oc et rtype
-> m (rtype rule term oc, Maybe (Path rule term oc))
rest' (RESTState m rule term oc et rtype
state{ working :: [Path rule term oc]
working = [Path rule term oc]
remaining })
where
(path :: Path rule term oc
path@([Step rule term oc]
ts, PathTerm term
ptTerm HashSet (term, rule)
_), [Path rule term oc]
remaining) = forall (m :: * -> *). GetWork m rule term oc
ws [Path rule term oc]
paths ExploredTerms term oc m
et
lastOrdering :: oc
lastOrdering :: oc
lastOrdering = if forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Step rule term oc]
ts then forall c a (m :: * -> *). OCAlgebra c a m -> c
top OCAlgebra oc term m
ocImpl else forall rule term a. Step rule term a -> a
ordering forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last [Step rule term oc]
ts
tsTerms :: [term]
tsTerms :: [term]
tsTerms = forall rule term a. Path rule term a -> [term]
pathTerms Path rule term oc
path
liftSet :: S.HashSet a -> ListT m a
liftSet :: forall a. HashSet a -> ListT m a
liftSet HashSet a
s = forall (m :: * -> *) a. m [a] -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. HashSet a -> [a]
S.toList HashSet a
s
candidates :: S.HashSet rule -> m (S.HashSet (term, rule))
candidates :: HashSet rule -> m (HashSet (term, rule))
candidates HashSet rule
rules = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList m [(term, rule)]
res
where
res :: m [(term, rule)]
res :: m [(term, rule)]
res = forall (m :: * -> *) a. ListT m a -> m [a]
runListT forall a b. (a -> b) -> a -> b
$ do
rule
r <- forall a. HashSet a -> ListT m a
liftSet HashSet rule
rules
term
t' <- forall (m :: * -> *) a. m [a] -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall a. HashSet a -> [a]
S.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) rule term.
RewriteRule m rule term =>
term -> rule -> m (HashSet term)
apply term
ptTerm rule
r
forall (m :: * -> *) a. Monad m => a -> m a
return (term
t', rule
r)
accepted :: S.HashSet (term, rule) -> m (M.HashMap term oc)
accepted :: HashSet (term, rule) -> m (HashMap term oc)
accepted HashSet (term, rule)
userRWs = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ListT m a -> m [a]
runListT (do
term
t' <- forall a. HashSet a -> ListT m a
liftSet forall a b. (a -> b) -> a -> b
$ forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map forall a b. (a, b) -> a
fst HashSet (term, rule)
userRWs
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
L.notElem term
t' [term]
tsTerms
let ord :: oc
ord = forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra oc term m
ocImpl oc
lastOrdering term
ptTerm term
t'
Bool
ok <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
isSat OCAlgebra oc term m
ocImpl oc
ord
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ok
forall (m :: * -> *) a. Monad m => a -> m a
return (term
t', oc
ord))
go :: HashSet (term, rule)
-> HashSet (term, rule)
-> HashMap term oc
-> m (rtype rule term oc, Maybe (Path rule term oc))
go HashSet (term, rule)
evalRWs HashSet (term, rule)
userRWs HashMap term oc
acceptedUserRewrites =
do
[Path rule term oc]
ep <- forall {rule}. m [([Step rule term oc], PathTerm rule term)]
evalPaths
[Path rule term oc]
up <- forall {rule}. m [([Step rule term oc], PathTerm rule term)]
userPaths
RESTState m rule term oc et rtype
-> m (rtype rule term oc, Maybe (Path rule term oc))
rest' (forall {et}.
[Path rule term oc] -> RESTState m rule term oc et rtype
state' ([Path rule term oc]
ep forall a. [a] -> [a] -> [a]
++ [Path rule term oc]
up))
where
state' :: [Path rule term oc] -> RESTState m rule term oc et rtype
state' [Path rule term oc]
p' = RESTState m rule term oc et rtype
state
{ working :: [Path rule term oc]
working = [Path rule term oc]
p' forall a. [a] -> [a] -> [a]
++ [Path rule term oc]
remaining
, finished :: rtype rule term oc
finished = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Path rule term oc]
p' then forall (a :: * -> * -> * -> *) oc rule term.
(RESTResult a, Hashable oc, Eq oc, Hashable rule, Eq rule,
Hashable term, Eq term) =>
Path rule term oc -> a rule term oc -> a rule term oc
includeInResult ([Step rule term oc]
ts, PathTerm rule term
pt) rtype rule term oc
fin else rtype rule term oc
fin
, explored :: ExploredTerms term oc m
explored =
let
deps :: HashSet term
deps = forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map forall a b. (a, b) -> a
fst (forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet (term, rule)
evalRWs HashSet (term, rule)
userRWs)
in
forall term c (m :: * -> *).
(Eq term, Hashable term) =>
term
-> c
-> HashSet term
-> ExploredTerms term c m
-> ExploredTerms term c m
ET.insert term
ptTerm oc
lastOrdering HashSet term
deps ExploredTerms term oc m
et
, targetPath :: Maybe (Path rule term oc)
targetPath =
if forall a. a -> Maybe a
Just term
ptTerm forall a. Eq a => a -> a -> Bool
== Maybe term
target then
case Maybe (Path rule term oc)
targetPath of
Just ([Step rule term oc]
tp, PathTerm rule term
_) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step rule term oc]
tp forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step rule term oc]
ts -> Maybe (Path rule term oc)
targetPath
Maybe (Path rule term oc)
_ -> forall a. a -> Maybe a
Just ([Step rule term oc]
ts, PathTerm rule term
pt)
else
Maybe (Path rule term oc)
targetPath
}
pt :: PathTerm rule term
pt = forall rule term.
term -> HashSet (term, rule) -> PathTerm rule term
PathTerm term
ptTerm HashSet (term, rule)
rejectedUserRewrites
rejectedUserRewrites :: S.HashSet (term, rule)
rejectedUserRewrites :: HashSet (term, rule)
rejectedUserRewrites = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ do
(term
t', rule
r) <- forall a. HashSet a -> [a]
S.toList HashSet (term, rule)
userRWs
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
L.notElem term
t' [term]
tsTerms
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
Mb.isNothing forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup term
t' HashMap term oc
acceptedUserRewrites
forall (m :: * -> *) a. Monad m => a -> m a
return (term
t', rule
r)
evalPaths :: m [([Step rule term oc], PathTerm rule term)]
evalPaths = forall (m :: * -> *) a. ListT m a -> m [a]
runListT forall a b. (a -> b) -> a -> b
$ do
(term
t', rule
r) <- forall (m :: * -> *) a. m [a] -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. HashSet a -> [a]
S.toList HashSet (term, rule)
evalRWs)
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
L.notElem term
t' [term]
tsTerms
let ord :: oc
ord = forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra oc term m
ocImpl oc
lastOrdering term
ptTerm term
t'
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall term c (m :: * -> *).
(Monad m, Eq term, Hashable term, Eq c, Show c, Hashable c) =>
term -> c -> ExploredTerms term c m -> m Bool
shouldExplore term
t' oc
ord ExploredTerms term oc m
et) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *). Alternative f => Bool -> f ()
guard
forall (m :: * -> *) a. Monad m => a -> m a
return ([Step rule term oc]
ts forall a. [a] -> [a] -> [a]
++ [forall rule term a.
PathTerm rule term -> rule -> a -> Bool -> Step rule term a
Step PathTerm rule term
pt rule
r oc
ord Bool
True], forall rule term.
term -> HashSet (term, rule) -> PathTerm rule term
PathTerm term
t' forall a. HashSet a
S.empty)
userPaths :: m [([Step rule term oc], PathTerm rule term)]
userPaths = forall (m :: * -> *) a. ListT m a -> m [a]
runListT forall a b. (a -> b) -> a -> b
$ do
(term
t', rule
r) <- forall a. HashSet a -> ListT m a
liftSet HashSet (term, rule)
userRWs
oc
ord <- forall (m :: * -> *) a. m [a] -> ListT m a
ListT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> [a]
Mb.maybeToList forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup term
t' HashMap term oc
acceptedUserRewrites
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall term c (m :: * -> *).
(Monad m, Eq term, Hashable term, Eq c, Show c, Hashable c) =>
term -> c -> ExploredTerms term c m -> m Bool
shouldExplore term
t' oc
ord ExploredTerms term oc m
et) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (f :: * -> *). Alternative f => Bool -> f ()
guard
forall (m :: * -> *) a. Monad m => a -> m a
return ([Step rule term oc]
ts forall a. [a] -> [a] -> [a]
++ [forall rule term a.
PathTerm rule term -> rule -> a -> Bool -> Step rule term a
Step PathTerm rule term
pt rule
r oc
ord Bool
False], forall rule term.
term -> HashSet (term, rule) -> PathTerm rule term
PathTerm term
t' forall a. HashSet a
S.empty)