{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# OPTIONS_GHC -Wno-error=deprecations #-}

module Language.REST.Rest (
    rest
  , pathsResult
  , termsResult
  , terms
  , PathsResult(..)
  , WorkStrategy(..)
  , RESTParams(..)
  ) where

import           Control.Monad
import           Control.Monad.List
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.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 :: PathsResult rule term oc
pathsResult = HashSet (Path rule term oc) -> PathsResult rule term oc
forall rule term oc.
HashSet (Path rule term oc) -> PathsResult rule term oc
PathsResult HashSet (Path rule term oc)
forall a. HashSet a
S.empty

termsResult :: TermsResult rule term oc
termsResult :: TermsResult rule term oc
termsResult = HashSet term -> TermsResult rule term oc
forall rule term oc. HashSet term -> TermsResult rule term oc
TermsResult HashSet term
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
  terms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term

instance RESTResult PathsResult where
  includeInResult :: 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) = HashSet (Path rule term oc) -> PathsResult rule term oc
forall rule term oc.
HashSet (Path rule term oc) -> PathsResult rule term oc
PathsResult (Path rule term oc
-> HashSet (Path rule term oc) -> HashSet (Path rule term oc)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Path rule term oc
p HashSet (Path rule term oc)
s)
  terms :: PathsResult rule term oc -> HashSet term
terms (PathsResult HashSet (Path rule term oc)
s) = [term] -> HashSet term
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((Path rule term oc -> [term]) -> [Path rule term oc] -> [term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Path rule term oc -> [term]
forall rule term a. Path rule term a -> [term]
pathTerms ([Path rule term oc] -> [term]) -> [Path rule term oc] -> [term]
forall a b. (a -> b) -> a -> b
$ HashSet (Path rule term oc) -> [Path rule term oc]
forall a. HashSet a -> [a]
S.toList HashSet (Path rule term oc)
s)


instance RESTResult TermsResult where
  includeInResult :: Path rule term oc
-> TermsResult rule term oc -> TermsResult rule term oc
includeInResult Path rule term oc
p (TermsResult HashSet term
s) = HashSet term -> TermsResult rule term oc
forall rule term oc. HashSet term -> TermsResult rule term oc
TermsResult (HashSet term -> HashSet term -> HashSet term
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet term
s ([term] -> HashSet term
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([term] -> HashSet term) -> [term] -> HashSet term
forall a b. (a -> b) -> a -> b
$ Path rule term oc -> [term]
forall rule term a. Path rule term a -> [term]
pathTerms Path rule term oc
p))
  terms :: TermsResult rule term oc -> HashSet term
terms (TermsResult HashSet term
s)             = HashSet term
s


data RESTState m rule term oc et rtype = RESTState
  { RESTState m rule term oc et rtype -> rtype rule term oc
finished   :: rtype rule term oc
  , RESTState m rule term oc et rtype -> [Path rule term oc]
working    :: [Path rule term oc]
  , RESTState m rule term oc et rtype -> ExploredTerms term oc m
explored   :: ExploredTerms term oc m
  , 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
  { RESTParams m rule term oc rtype -> HashSet rule
re           :: S.HashSet rule
  , RESTParams m rule term oc rtype -> HashSet rule
ru           :: S.HashSet rule
  , RESTParams m rule term oc rtype -> Maybe term
target       :: Maybe term
  , RESTParams m rule term oc rtype -> WorkStrategy rule term oc
workStrategy :: WorkStrategy rule term oc
  , RESTParams m rule term oc rtype -> OCAlgebra oc term m
ocImpl       :: OCAlgebra oc term m
  , RESTParams m rule term oc rtype -> rtype rule term oc
initRes      :: rtype rule term oc
  , 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 :: 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 =
  RESTState m rule term oc Any rtype
-> m (rtype rule term oc, Maybe (Path rule term oc))
forall (rtype :: * -> * -> * -> *) et.
RESTResult rtype =>
RESTState m rule term oc et rtype
-> m (rtype rule term oc, Maybe (Path rule term oc))
rest' (rtype rule term oc
-> [Path rule term oc]
-> ExploredTerms term oc m
-> Maybe (Path rule term oc)
-> RESTState m rule term oc Any rtype
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 [([], term -> HashSet (term, rule) -> PathTerm rule term
forall rule term.
term -> HashSet (term, rule) -> PathTerm rule term
PathTerm term
t HashSet (term, rule)
forall a. HashSet a
S.empty)] ExploredTerms term oc m
initET Maybe (Path rule term oc)
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 = ExploreFuncs term oc m
-> ExploreStrategy -> ExploredTerms term oc m
forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ET.empty ((oc -> oc -> oc)
-> (oc -> oc -> m Bool)
-> (oc -> term -> term -> oc)
-> ExploreFuncs term oc m
forall term c (m :: * -> *).
(c -> c -> c)
-> (c -> c -> m Bool)
-> (c -> term -> term -> c)
-> ExploreFuncs term c m
EF (OCAlgebra oc term m -> oc -> oc -> oc
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
AC.union OCAlgebra oc term m
ocImpl) (OCAlgebra oc term m -> oc -> oc -> m Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
AC.notStrongerThan OCAlgebra oc term m
ocImpl) (OCAlgebra oc term m -> oc -> term -> term -> oc
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)            = (rtype rule term oc, Maybe (Path rule term oc))
-> m (rtype rule term oc, Maybe (Path rule term oc))
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) <- GetWork m rule term oc
forall (m :: * -> *). GetWork m rule term oc
ws [Path rule term oc]
paths ExploredTerms term oc m
et
      , [Step rule term oc] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step rule term oc]
steps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [Step rule term oc] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Path rule term oc -> [Step rule term oc]
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 <- term -> oc -> ExploredTerms term oc m -> m Bool
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) = GetWork m rule term oc
forall (m :: * -> *). GetWork m rule term oc
ws [Path rule term oc]
paths ExploredTerms term oc m
et

        lastOrdering :: oc
        lastOrdering :: oc
lastOrdering = if [Step rule term oc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
L.null [Step rule term oc]
ts then OCAlgebra oc term m -> oc
forall c a (m :: * -> *). OCAlgebra c a m -> c
top OCAlgebra oc term m
ocImpl else Step rule term oc -> oc
forall rule term a. Step rule term a -> a
ordering (Step rule term oc -> oc) -> Step rule term oc -> oc
forall a b. (a -> b) -> a -> b
$ [Step rule term oc] -> Step rule term oc
forall a. [a] -> a
last [Step rule term oc]
ts

        tsTerms :: [term]
        tsTerms :: [term]
tsTerms = Path rule term oc -> [term]
forall rule term a. Path rule term a -> [term]
pathTerms Path rule term oc
path

        liftSet :: S.HashSet a -> ListT m a
        liftSet :: HashSet a -> ListT m a
liftSet HashSet a
s = m [a] -> ListT m a
forall (m :: * -> *) a. m [a] -> ListT m a
ListT (m [a] -> ListT m a) -> m [a] -> ListT m a
forall a b. (a -> b) -> a -> b
$ [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> m [a]) -> [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ HashSet a -> [a]
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 = ([(term, rule)] -> HashSet (term, rule))
-> m [(term, rule)] -> m (HashSet (term, rule))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(term, rule)] -> HashSet (term, rule)
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 = ListT m (term, rule) -> m [(term, rule)]
forall (m :: * -> *) a. ListT m a -> m [a]
runListT (ListT m (term, rule) -> m [(term, rule)])
-> ListT m (term, rule) -> m [(term, rule)]
forall a b. (a -> b) -> a -> b
$ do
              rule
r   <- HashSet rule -> ListT m rule
forall a. HashSet a -> ListT m a
liftSet HashSet rule
rules
              term
t'  <- m [term] -> ListT m term
forall (m :: * -> *) a. m [a] -> ListT m a
ListT (m [term] -> ListT m term) -> m [term] -> ListT m term
forall a b. (a -> b) -> a -> b
$ HashSet term -> [term]
forall a. HashSet a -> [a]
S.toList (HashSet term -> [term]) -> m (HashSet term) -> m [term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> rule -> m (HashSet term)
forall (m :: * -> *) rule term.
RewriteRule m rule term =>
term -> rule -> m (HashSet term)
apply term
ptTerm rule
r
              (term, rule) -> ListT m (term, rule)
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 = [(term, oc)] -> HashMap term oc
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(term, oc)] -> HashMap term oc)
-> m [(term, oc)] -> m (HashMap term oc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ListT m (term, oc) -> m [(term, oc)]
forall (m :: * -> *) a. ListT m a -> m [a]
runListT (ListT m (term, oc) -> m [(term, oc)])
-> ListT m (term, oc) -> m [(term, oc)]
forall a b. (a -> b) -> a -> b
$ do
          term
t' <- HashSet term -> ListT m term
forall a. HashSet a -> ListT m a
liftSet (HashSet term -> ListT m term) -> HashSet term -> ListT m term
forall a b. (a -> b) -> a -> b
$ ((term, rule) -> term) -> HashSet (term, rule) -> HashSet term
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (term, rule) -> term
forall a b. (a, b) -> a
fst HashSet (term, rule)
userRWs
          Bool -> ListT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT m ()) -> Bool -> ListT m ()
forall a b. (a -> b) -> a -> b
$ term -> [term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
L.notElem term
t' [term]
tsTerms
          let ord :: oc
ord = OCAlgebra oc term m -> oc -> term -> term -> oc
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 <- m Bool -> ListT m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m Bool -> ListT m Bool) -> m Bool -> ListT m Bool
forall a b. (a -> b) -> a -> b
$ OCAlgebra oc term m -> oc -> m Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
isSat OCAlgebra oc term m
ocImpl oc
ord
          Bool -> ListT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
ok
          (term, oc) -> ListT m (term, oc)
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 <- m [Path rule term oc]
forall rule. m [([Step rule term oc], PathTerm rule term)]
evalPaths
            [Path rule term oc]
up <- m [Path rule term oc]
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' ([Path rule term oc] -> RESTState m rule term oc et rtype
forall et. [Path rule term oc] -> RESTState m rule term oc et rtype
state' ([Path rule term oc]
ep [Path rule term oc] -> [Path rule term oc] -> [Path rule term oc]
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' [Path rule term oc] -> [Path rule term oc] -> [Path rule term oc]
forall a. [a] -> [a] -> [a]
++ [Path rule term oc]
remaining
              , finished :: rtype rule term oc
finished = if [Path rule term oc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Path rule term oc]
p' then Path rule term oc -> rtype rule term oc -> rtype rule term oc
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 = ((term, rule) -> term) -> HashSet (term, rule) -> HashSet term
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
S.map (term, rule) -> term
forall a b. (a, b) -> a
fst (HashSet (term, rule)
-> HashSet (term, rule) -> HashSet (term, rule)
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet (term, rule)
evalRWs HashSet (term, rule)
userRWs)
                  in
                    term
-> oc
-> HashSet term
-> ExploredTerms term oc m
-> ExploredTerms term oc m
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 term -> Maybe term
forall a. a -> Maybe a
Just term
ptTerm Maybe term -> Maybe term -> Bool
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
_) | [Step rule term oc] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step rule term oc]
tp Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Step rule term oc] -> Int
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)
_                                     -> Path rule term oc -> 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 = term -> HashSet (term, rule) -> PathTerm rule term
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 = [(term, rule)] -> HashSet (term, rule)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(term, rule)] -> HashSet (term, rule))
-> [(term, rule)] -> HashSet (term, rule)
forall a b. (a -> b) -> a -> b
$ do
              (term
t', rule
r) <- HashSet (term, rule) -> [(term, rule)]
forall a. HashSet a -> [a]
S.toList HashSet (term, rule)
userRWs
              Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ term -> [term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
L.notElem term
t' [term]
tsTerms
              Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Maybe oc -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (Maybe oc -> Bool) -> Maybe oc -> Bool
forall a b. (a -> b) -> a -> b
$ term -> HashMap term oc -> Maybe oc
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup term
t' HashMap term oc
acceptedUserRewrites
              (term, rule) -> [(term, rule)]
forall (m :: * -> *) a. Monad m => a -> m a
return (term
t', rule
r)


            evalPaths :: m [([Step rule term oc], PathTerm rule term)]
evalPaths = ListT m ([Step rule term oc], PathTerm rule term)
-> m [([Step rule term oc], PathTerm rule term)]
forall (m :: * -> *) a. ListT m a -> m [a]
runListT (ListT m ([Step rule term oc], PathTerm rule term)
 -> m [([Step rule term oc], PathTerm rule term)])
-> ListT m ([Step rule term oc], PathTerm rule term)
-> m [([Step rule term oc], PathTerm rule term)]
forall a b. (a -> b) -> a -> b
$ do
              (term
t', rule
r) <- m [(term, rule)] -> ListT m (term, rule)
forall (m :: * -> *) a. m [a] -> ListT m a
ListT (m [(term, rule)] -> ListT m (term, rule))
-> m [(term, rule)] -> ListT m (term, rule)
forall a b. (a -> b) -> a -> b
$ [(term, rule)] -> m [(term, rule)]
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet (term, rule) -> [(term, rule)]
forall a. HashSet a -> [a]
S.toList HashSet (term, rule)
evalRWs)
              Bool -> ListT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> ListT m ()) -> Bool -> ListT m ()
forall a b. (a -> b) -> a -> b
$ term -> [term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
L.notElem term
t' [term]
tsTerms
              let ord :: oc
ord = OCAlgebra oc term m -> oc -> term -> term -> oc
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine OCAlgebra oc term m
ocImpl oc
lastOrdering term
ptTerm term
t'
              m Bool -> ListT m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (term -> oc -> ExploredTerms term oc m -> m Bool
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) ListT m Bool -> (Bool -> ListT m ()) -> ListT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> ListT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard
              ([Step rule term oc], PathTerm rule term)
-> ListT m ([Step rule term oc], PathTerm rule term)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Step rule term oc]
ts [Step rule term oc] -> [Step rule term oc] -> [Step rule term oc]
forall a. [a] -> [a] -> [a]
++ [PathTerm rule term -> rule -> oc -> Bool -> Step rule term oc
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], term -> HashSet (term, rule) -> PathTerm rule term
forall rule term.
term -> HashSet (term, rule) -> PathTerm rule term
PathTerm term
t' HashSet (term, rule)
forall a. HashSet a
S.empty)

            userPaths :: m [([Step rule term oc], PathTerm rule term)]
userPaths = ListT m ([Step rule term oc], PathTerm rule term)
-> m [([Step rule term oc], PathTerm rule term)]
forall (m :: * -> *) a. ListT m a -> m [a]
runListT (ListT m ([Step rule term oc], PathTerm rule term)
 -> m [([Step rule term oc], PathTerm rule term)])
-> ListT m ([Step rule term oc], PathTerm rule term)
-> m [([Step rule term oc], PathTerm rule term)]
forall a b. (a -> b) -> a -> b
$ do
              (term
t', rule
r) <- HashSet (term, rule) -> ListT m (term, rule)
forall a. HashSet a -> ListT m a
liftSet HashSet (term, rule)
userRWs
              oc
ord <- m [oc] -> ListT m oc
forall (m :: * -> *) a. m [a] -> ListT m a
ListT (m [oc] -> ListT m oc) -> m [oc] -> ListT m oc
forall a b. (a -> b) -> a -> b
$ [oc] -> m [oc]
forall (m :: * -> *) a. Monad m => a -> m a
return ([oc] -> m [oc]) -> [oc] -> m [oc]
forall a b. (a -> b) -> a -> b
$ Maybe oc -> [oc]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe oc -> [oc]) -> Maybe oc -> [oc]
forall a b. (a -> b) -> a -> b
$ term -> HashMap term oc -> Maybe oc
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup term
t' HashMap term oc
acceptedUserRewrites
              m Bool -> ListT m Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (term -> oc -> ExploredTerms term oc m -> m Bool
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) ListT m Bool -> (Bool -> ListT m ()) -> ListT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> ListT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard
              ([Step rule term oc], PathTerm rule term)
-> ListT m ([Step rule term oc], PathTerm rule term)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Step rule term oc]
ts [Step rule term oc] -> [Step rule term oc] -> [Step rule term oc]
forall a. [a] -> [a] -> [a]
++ [PathTerm rule term -> rule -> oc -> Bool -> Step rule term oc
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], term -> HashSet (term, rule) -> PathTerm rule term
forall rule term.
term -> HashSet (term, rule) -> PathTerm rule term
PathTerm term
t' HashSet (term, rule)
forall a. HashSet a
S.empty)