{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE NamedFieldPuns #-}
{-# OPTIONS_GHC -Wno-error=deprecations #-}

-- | This module contains the core REST algorithm
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

-- | The set of all 'Path's explored by REST.
newtype PathsResult rule term oc = PathsResult (S.HashSet (Path rule term oc))

-- | The set of all terms explored by REST.
newtype TermsResult rule term oc = TermsResult (S.HashSet term)

-- | An initial (empty) instance of 'PathsResult'
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

-- | An initial (empty) instance of 'TermsResult'
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

--  | This class encapsulates the mechanism for REST to store the result of its computation.
-- For example, we include two instances: 'PathsResult', which stores each 'Path' generated
-- by REST (useful for debugging and visualization); and 'TermsResult', which only stores the
-- resulting terms (which uses less memory and is likely more performant).
class RESTResult a where
  -- | Includes a term in the result
  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
  -- | Obtains the terms explored by REST
  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 params terms@ performs the REST search from initial term @term@ with parameters@params@.
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)