{-# 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 = 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

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

--  | 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) = 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 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 :: 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)