{-# 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 = 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 :: forall rule term oc. 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
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) = 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)
resultTerms :: forall term rule oc.
(Eq term, Hashable term) =>
PathsResult rule term oc -> HashSet term
resultTerms (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 :: 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) = 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 => 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))
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 :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> HashSet rule
re :: HashSet rule
re,HashSet rule
ru :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> HashSet rule
ru :: HashSet rule
ru,OCAlgebra oc term m
ocImpl :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> OCAlgebra oc term m
ocImpl :: OCAlgebra oc term m
ocImpl,WorkStrategy rule term oc
workStrategy :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> WorkStrategy rule term oc
workStrategy :: WorkStrategy rule term oc
workStrategy,rtype rule term oc
initRes :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> rtype rule term oc
initRes :: rtype rule term oc
initRes,Maybe term
target :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> Maybe term
target :: Maybe term
target,ExploreStrategy
etStrategy :: forall (m :: * -> *) rule term oc (rtype :: * -> * -> * -> *).
RESTParams m rule term oc rtype -> ExploreStrategy
etStrategy :: 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 a. a -> m a
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 a. [a] -> 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 a. [a] -> 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 = 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 = 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 a. [a] -> 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. HasCallStack => [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 :: forall a. 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 a. 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 a b. (a -> b) -> m a -> m b
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 a. a -> ListT m a
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 (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 (m :: * -> *) a. Monad m => m a -> ListT m a
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 a. a -> ListT m a
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 = p' ++ remaining
, finished = if null p' then includeInResult (ts, pt) fin else fin
, explored =
let
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 => HashSet a -> HashSet a -> HashSet a
S.union HashSet (term, rule)
evalRWs HashSet (term, rule)
userRWs)
in
ET.insert ptTerm lastOrdering deps et
, targetPath =
if Just ptTerm == target then
case targetPath of
Just ([Step rule term oc]
tp, PathTerm rule term
_) | [Step rule term oc] -> Int
forall a. [a] -> 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 a. [a] -> 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
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 a. a -> [a]
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 a. a -> m a
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 (m :: * -> *) a. Monad m => m a -> ListT m a
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 a b. ListT m a -> (a -> ListT m b) -> ListT m b
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 a. a -> ListT m a
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 a. a -> m a
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 (m :: * -> *) a. Monad m => m a -> ListT m a
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 a b. ListT m a -> (a -> ListT m b) -> ListT m b
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 a. a -> ListT m a
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)