Explored Terms optimization (#20)

* Explore optimization

* Various changes for exploration optimization

* Remove unused

.gitignore

@@ -2,3 +2,4 @@ graphs/*
 .stack-work
 dist-newstyle
 .DS_Store
+*.tar.gz

rest-rewrite.cabal

@@ -25,6 +25,7 @@ library
     Language.REST.Internal.MultiSet
     Language.REST.Internal.MultisetOrder
     Language.REST.Internal.OpOrdering
+    Language.REST.Internal.Orphans
     Language.REST.Internal.PartialOrder
     Language.REST.Internal.Rewrite
     Language.REST.Internal.Util
@@ -51,7 +52,7 @@ library
   hs-source-dirs: src
   build-depends:  base                 >= 4.7 && < 5
                 , containers           >= 0.6.2 && < 0.7
-                , hashable             >= 1.3.4 && < 1.4
+                , hashable             >= 1.3.0 && < 1.4
                 , process              >= 1.6.9 && < 1.7
                 , parsec               >= 3.1.14 && < 3.2
                 , mtl                  >= 2.2.2 && < 2.3
@@ -98,6 +99,7 @@ Test-Suite test-rest
                 , rest-rewrite
                 , testlib
   other-modules:
+    ExploredTerms
     KBO
     LazyOC
     MultisetOrder

src/Language/REST/ExploredTerms.hs

@@ -24,33 +24,29 @@ import Prelude hiding (lookup)
 data ExploreStrategy =
   ExploreAlways | ExploreLessConstrained | ExploreWhenNeeded | ExploreOnce
 
-data ExploreFuncs c m = EF
+data ExploreFuncs term c m = EF
   { union           :: c -> c -> c
     -- | @c0 `subsumes` c1@ if @c0@ permits all orderings permited by @c1@
   , subsumes        :: c -> c -> m Bool
+  , exRefine        :: c -> term -> term -> c
   }
 
 -- A mapping of terms, to the rewritten terms that need to be fully explored
 -- in order for this term to be fully explored
 data ExploredTerms term c m =
-  ET (M.HashMap term (c, (S.HashSet term))) (ExploreFuncs c m) ExploreStrategy
-
-trace' :: String -> b -> b
--- trace' = trace
-trace' _ x = x
-
+  ET (M.HashMap term (c, (S.HashSet term))) (ExploreFuncs term c m) ExploreStrategy
 
 size :: ExploredTerms term c m -> Int
 size (ET m _ _) = M.size m
 
-empty :: ExploreFuncs c m -> ExploreStrategy -> ExploredTerms term c m
+empty :: ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
 empty = ET M.empty
 
 visited :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Bool
 visited t (ET m _ _) = M.member t m
 
 insert :: (Eq term, Hashable term) => term -> c -> S.HashSet term -> ExploredTerms term c m -> ExploredTerms term c m
-insert t oc s (ET etMap ef@(EF union _ ) strategy) = ET (M.insertWith go t (oc, s) etMap) ef strategy
+insert t oc s (ET etMap ef@(EF union _ _) strategy) = ET (M.insertWith go t (oc, s) etMap) ef strategy
   where
     go (oc1, s1) (oc2, s2) = (union oc1 oc2, S.union s1 s2)
 
@@ -59,31 +55,41 @@ lookup t (ET etMap _ _) = M.lookup t etMap
 
 -- | @isFullyExplored t c M = not explorable(t, c)@ where @explorable@ is
 -- defined as in the REST paper.
-isFullyExplored :: forall term c m . (Monad m, Show term, Eq term, Hashable term, Eq c) =>
+isFullyExplored :: forall term c m . (Monad m, Eq term, Hashable term, Hashable c, Eq c, Show c) =>
   term -> c -> ExploredTerms term c m -> m Bool
-isFullyExplored t0 oc0 et@(ET _ (EF{subsumes}) _) = result where
+isFullyExplored t0 oc0 et@(ET _ (EF{subsumes,exRefine}) _) = result where
 
-  result = go S.empty [t0]
-    -- if (trace ("Check " ++ show t0) go) S.empty [t0]
-    -- then trace (show t0 ++ " is fully explored.") True
-    -- else False
+  result = go S.empty [(t0, oc0)]
 
-  go :: S.HashSet term -> [term] -> m Bool
+  -- Arg 1: Steps that have already been seen
+  -- Arg 2: Steps to consider
+  go :: S.HashSet (term, c) -> [(term, c)] -> m Bool
+
+  -- Completed worklist, this term is fully explored at these constraints
   go _ []       = return True
-  go seen (h:t) | Just (oc, trms) <- lookup h et
+
+  -- Term `h` has been seen before at constraints `oc`
+  go seen ((h, oc'):rest) | Just (oc, trms) <- lookup h et
                 = do
-                    haveExploredAllCurrentlyPermitedOrderings <- oc `subsumes` oc0
-                    if haveExploredAllCurrentlyPermitedOrderings
-                      then go seen' t
+                    exploringPathWouldNotPermitDifferentSteps <- oc `subsumes` oc'
+                    if exploringPathWouldNotPermitDifferentSteps
+                      then go seen' rest
                       else
-                        let ts = (S.union trms (S.fromList t)) `S.difference` seen'
-                        in go seen' (S.toList ts)
+                        let
+                          -- Exploring `h` at these constraints
+                          -- would allow exploration of each t in trms,
+                          -- at the constraints generated by the step from h to t
+                          trms' = S.map (\t -> (t, exRefine oc' h t)) trms
+                          ts    = (S.union trms' (S.fromList rest)) `S.difference` seen'
+                        in
+                          go seen' (S.toList ts)
                   where
-                    seen' = S.insert h seen
+                    seen' = S.insert (h, oc') seen
 
-  go _ _        | otherwise = trace' "GF" $ return False -- trace ("Must check " ++ show t0 ++ " . Visited: " ++ (show $ visited t0 et)) False
+  -- There exists a reachable term that has never previously been seen; not fully explored
+  go _ _        | otherwise = return False
 
-shouldExplore :: forall term c m . (Monad m, Show term, Eq term, Hashable term, Eq c, Show c) =>
+shouldExplore :: 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 t oc et@(ET _ EF{subsumes} strategy) =
   case strategy of
@@ -94,7 +100,5 @@ shouldExplore t oc et@(ET _ EF{subsumes} strategy) =
       case lookup t et of
         Just (oc', _) -> do
           s <- oc' `subsumes` oc
-          return  $ if s
-            then trace' ((show oc') ++ " subsumes " ++ (show oc)) False
-            else True
+          return $ not s
         Nothing       -> return True

src/Language/REST/Internal/EquivalenceClass.hs

@@ -1,5 +1,9 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
 
 module Language.REST.Internal.EquivalenceClass
     ( isMember
@@ -26,7 +30,16 @@ import Language.REST.Types () -- Hashable (S.Set a)
 -- | Equivalent classes of the @(==)@ relation of a type @a@.
 newtype EquivalenceClass a =
   -- | The set contains all of the elements of the class
-  EquivalenceClass (S.Set a) deriving (Ord, Eq, Generic, Hashable)
+  EquivalenceClass (S.Set a)
+#if MIN_VERSION_hashable(1,3,5)
+  deriving (Ord, Eq, Generic, Hashable)
+#else
+  deriving (Ord, Eq, Generic)
+#endif
+
+#if !MIN_VERSION_hashable(1,3,5)
+deriving instance Hashable (S.Set a) => Hashable (EquivalenceClass a)
+#endif
 
 instance Show a => Show (EquivalenceClass a) where
     show (EquivalenceClass xs) = L.intercalate " = " (map show (S.toList xs)) 

src/Language/REST/Internal/Orphans.hs

@@ -0,0 +1,33 @@
+{-# LANGUAGE CPP #-}
+
+module Language.REST.Internal.Orphans where
+
+#if !MIN_VERSION_hashable(1,3,5)
+import Data.Hashable
+import Data.Hashable.Lifted
+import Data.Set as Set
+import Data.Map as Map
+
+instance Hashable1 Set where
+    liftHashWithSalt h s x = Set.foldl' h (hashWithSalt s (Set.size x)) x
+
+instance (Hashable a) => Hashable (Set a) where
+  hashWithSalt = hashWithSalt1
+
+instance Hashable2 Map.Map where
+    liftHashWithSalt2 hk hv s m = Map.foldlWithKey'
+        (\s' k v -> hv (hk s' k) v)
+        (hashWithSalt s (Map.size m))
+        m
+
+instance Hashable k => Hashable1 (Map.Map k) where
+    liftHashWithSalt h s m = Map.foldlWithKey'
+        (\s' k v -> h (hashWithSalt s' k) v)
+        (hashWithSalt s (Map.size m))
+        m
+
+-- | @since 1.3.4.0
+instance (Hashable k, Hashable v) => Hashable (Map.Map k v) where
+    hashWithSalt = hashWithSalt2
+
+#endif

src/Language/REST/Internal/PartialOrder.hs

@@ -23,6 +23,7 @@ import qualified Data.Map as M
 import qualified Data.List as L
 
 import Language.REST.Types () -- Hashable (M.Map a b)
+import Language.REST.Internal.Orphans ()
 import Text.Printf
 
 -- | Irreflexive (strict) partial orders

src/Language/REST/Internal/WQO.hs

@@ -35,6 +35,7 @@ import qualified Data.Set as S
 
 import qualified Language.REST.Internal.EquivalenceClass as EC
 import qualified Language.REST.Internal.PartialOrder as PO
+import Language.REST.Internal.Orphans ()
 import Language.REST.Op
 import Language.REST.SMT
 

src/Language/REST/Internal/WorkStrategy.hs

@@ -9,30 +9,30 @@ import Language.REST.Internal.Rewrite
 import Data.Hashable
 import qualified Data.List as L
 
-type GetWork m rule term et oc = [Path rule term oc] -> (term -> et) -> ExploredTerms et oc m -> (Path rule term oc, [Path rule term oc])
+type GetWork m rule term oc = [Path rule term oc] -> ExploredTerms term oc m -> (Path rule term oc, [Path rule term oc])
 
-newtype WorkStrategy rule term et oc = WorkStrategy (forall m . GetWork m rule term et oc)
+newtype WorkStrategy rule term oc = WorkStrategy (forall m . GetWork m rule term oc)
 
-bfs :: WorkStrategy rule term et oc
+bfs :: WorkStrategy rule term oc
 bfs = WorkStrategy bfs'
 
-notVisitedFirst :: (Eq term, Eq rule, Eq oc, Eq et, Hashable et) => WorkStrategy rule term et oc
+notVisitedFirst :: (Eq term, Eq rule, Eq oc, Hashable term) => WorkStrategy rule term oc
 notVisitedFirst = WorkStrategy notVisitedFirst'
 
-bfs' :: [Path rule term oc] -> (term -> et) -> ExploredTerms et oc m -> (Path rule term oc, [Path rule term oc])
-bfs' (h:t) _ _ = (h, t)
-bfs' _ _ _ = error "empty path list"
+bfs' :: [Path rule term oc] ->  ExploredTerms et oc m -> (Path rule term oc, [Path rule term oc])
+bfs' (h:t) _ = (h, t)
+bfs' _ _ = error "empty path list"
 
-notVisitedFirst' :: (Eq term, Eq rule, Eq oc, Eq et, Hashable et) => GetWork m rule term et oc
-notVisitedFirst' paths toET et =
-  case L.find (\p -> not (ET.visited (toET $ runtimeTerm p) et)) paths of
+notVisitedFirst' :: (Eq term, Eq rule, Eq oc, Hashable term) => GetWork m rule term oc
+notVisitedFirst' paths et =
+  case L.find (\p -> not (ET.visited (runtimeTerm p) et)) paths of
     Just p  -> (p, L.delete p paths)
     Nothing -> (head paths, tail paths)
 
-commutesLast :: forall term oc et . (Eq term, Eq oc, Eq et, Hashable et) => WorkStrategy Rewrite term et oc
+commutesLast :: forall term oc . (Eq term, Eq oc, Hashable term) => WorkStrategy Rewrite term oc
 commutesLast = WorkStrategy go where
-  go paths toET et =
-    case L.find (\p -> not (ET.visited (toET $ runtimeTerm p) et || fromComm p)) paths of
+  go paths et =
+    case L.find (\p -> not (ET.visited (runtimeTerm p) et || fromComm p)) paths of
         Just p  -> (p, L.delete p paths)
         Nothing -> (head paths, tail paths)
   fromComm ([], _)    = False

src/Language/REST/Rest.hs

@@ -57,51 +57,47 @@ instance RESTResult TermsResult where
 data RESTState m rule term oc et rtype = RESTState
   { finished   :: rtype rule term oc
   , working    :: [Path rule term oc]
-  , explored   :: ExploredTerms et oc m
+  , explored   :: ExploredTerms term oc m
   , targetPath :: Maybe (Path rule term oc)
   }
 
-data RESTParams m rule term oc et rtype = RESTParams
+data RESTParams m rule term oc rtype = RESTParams
   { re           :: S.HashSet rule
   , ru           :: S.HashSet rule
-  , toET         :: term -> et
   , target       :: Maybe term
-  , workStrategy :: WorkStrategy rule term et oc
+  , workStrategy :: WorkStrategy rule term oc
   , ocImpl       :: OCAlgebra oc term m
   , initRes      :: rtype rule term oc
   , etStrategy   :: ExploreStrategy
   }
 
-rest :: forall m rule term oc et rtype .
+rest :: forall m rule term oc rtype .
   ( MonadIO m
   , RewriteRule m rule term
-  , Show et
   , Hashable term
   , Eq term
   , Hashable rule
-  , Hashable et
   , Hashable oc
   , Eq rule
-  , Eq et
   , Eq oc
   , Show oc
   , RESTResult rtype)
-  => RESTParams m rule term oc et rtype
+  => RESTParams m rule term oc rtype
   -> term
   -> m ((rtype rule term oc), Maybe (Path rule term oc))
-rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target,etStrategy} t =
+rest RESTParams{re,ru,ocImpl,workStrategy,initRes,target,etStrategy} t =
   rest' (RESTState initRes [([], PathTerm t S.empty)] initET Nothing)
   where
     (WorkStrategy ws) = workStrategy
-    initET = ET.empty (EF (AC.union ocImpl) (AC.notStrongerThan ocImpl)) etStrategy
+    initET = ET.empty (EF (AC.union ocImpl) (AC.notStrongerThan ocImpl) (refine ocImpl)) etStrategy
 
     rest' (RESTState fin [] _ targetPath)            = return (fin, targetPath)
     rest' state@(RESTState _   paths et (Just targetPath))
-      | ((steps, _), remaining) <- ws paths toET et
+      | ((steps, _), remaining) <- ws paths et
       , length steps >= length (fst targetPath)
       = rest' state{working = remaining}
     rest' state@(RESTState fin paths et targetPath) = do
-      se <- shouldExplore (toET ptTerm) lastOrdering et
+      se <- shouldExplore ptTerm lastOrdering et
       if se
         then do
           evalRWs <- candidates re
@@ -112,7 +108,7 @@ rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target,etStrategy} t =
           rest' (state{ working = remaining })
       where
 
-        (path@(ts, PathTerm ptTerm _), remaining) = ws paths toET et
+        (path@(ts, PathTerm ptTerm _), remaining) = ws paths et
 
         lastOrdering :: oc
         lastOrdering = if L.null ts then top ocImpl else ordering $ last ts
@@ -153,9 +149,9 @@ rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target,etStrategy} t =
               , finished = if null p' then includeInResult (ts, pt) fin else fin
               , explored =
                   let
-                    deps = S.map (toET . fst) (S.union evalRWs userRWs)
+                    deps = S.map fst (S.union evalRWs userRWs)
                   in
-                    ET.insert (toET ptTerm) lastOrdering deps et
+                    ET.insert ptTerm lastOrdering deps et
               , targetPath =
                 if Just ptTerm == target then
                   case targetPath of
@@ -180,11 +176,11 @@ rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target,etStrategy} t =
               (t', r) <- ListT $ return (S.toList evalRWs)
               guard $ L.notElem t' tsTerms
               let ord = refine ocImpl lastOrdering ptTerm t'
-              lift (shouldExplore (toET t') ord et) >>= guard
+              lift (shouldExplore t' ord et) >>= guard
               return (ts ++ [Step pt r ord True], PathTerm t' S.empty)
 
             userPaths = runListT $ do
               (t', r) <- liftSet userRWs
               ord <- ListT $ return $ Mb.maybeToList $ M.lookup t' acceptedUserRewrites
-              lift (shouldExplore (toET t') ord et) >>= guard
+              lift (shouldExplore t' ord et) >>= guard
               return (ts ++ [Step pt r ord False], PathTerm t' S.empty)

test/BagExample.hs

@@ -105,7 +105,6 @@ mkBagGraph =
       RESTParams
         { re           = S.empty
         , ru           = rules
-        , toET         = id
         , target       = Nothing
         , workStrategy = bfs
         , ocImpl       = impl