diff --git a/rest-rewrite.cabal b/rest-rewrite.cabal --- a/rest-rewrite.cabal +++ b/rest-rewrite.cabal @@ -1,12 +1,12 @@ name: rest-rewrite build-type: Simple -version: 0.2.0 +version: 0.3.0 cabal-version: 2.0 category: Rewriting maintainer: Zack Grannan author: Zack Grannan license: BSD3 -description: Rewriting library with online termination checking. +description: REST is a Rewriting library with online termination checking. For more details see the paper at https://arxiv.org/abs/2202.05872. synopsis: Rewriting library with online termination checking license-file: LICENSE @@ -25,6 +25,7 @@ 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 @@ -98,6 +99,7 @@ , rest-rewrite , testlib other-modules: + ExploredTerms KBO LazyOC MultisetOrder diff --git a/src/Language/REST/ExploredTerms.hs b/src/Language/REST/ExploredTerms.hs --- a/src/Language/REST/ExploredTerms.hs +++ b/src/Language/REST/ExploredTerms.hs @@ -1,5 +1,8 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-} +-- | This module implements the optimizations to prune the +-- exploration of rewrites of terms that have been already considered +-- (section 6.4 of the REST paper). module Language.REST.ExploredTerms ( ExploredTerms @@ -21,63 +24,72 @@ 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) lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, (S.HashSet term)) lookup t (ET etMap _ _) = M.lookup t etMap -isFullyExplored :: forall term c m . (Monad m, Show term, Eq term, Hashable term, Eq c) => +-- | @isFullyExplored t c M = not explorable(t, c)@ where @explorable@ is +-- defined as in the REST paper. +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 - ns <- oc `subsumes` oc0 - if ns - 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 @@ -88,7 +100,5 @@ 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 diff --git a/src/Language/REST/Internal/EquivalenceClass.hs b/src/Language/REST/Internal/EquivalenceClass.hs --- a/src/Language/REST/Internal/EquivalenceClass.hs +++ b/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 @@ -12,7 +16,6 @@ , head , EquivalenceClass , elems - , toPairs , isSubsetOf ) where @@ -24,9 +27,20 @@ import Language.REST.Types () -- Hashable (S.Set a) +-- | Equivalent classes of the @(==)@ relation of a type @a@. newtype EquivalenceClass a = - EquivalenceClass (S.Set a) deriving (Ord, Eq, Generic, Hashable) + -- | The set contains all of the elements of the class + 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)) @@ -61,15 +75,6 @@ toList :: EquivalenceClass a -> [a] toList (EquivalenceClass s) = S.toList s - -toPairs :: EquivalenceClass b -> [(b, b)] -toPairs e = - let - list = toList e - in - if length list < 2 - then [] - else zip list (tail list) {-# INLINE elems #-} elems :: EquivalenceClass a -> S.Set a diff --git a/src/Language/REST/Internal/Orphans.hs b/src/Language/REST/Internal/Orphans.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/Orphans.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE CPP #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Language.REST.Internal.Orphans() where + +#if !MIN_VERSION_hashable(1,3,4) +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 diff --git a/src/Language/REST/Internal/PartialOrder.hs b/src/Language/REST/Internal/PartialOrder.hs --- a/src/Language/REST/Internal/PartialOrder.hs +++ b/src/Language/REST/Internal/PartialOrder.hs @@ -23,9 +23,23 @@ import qualified Data.List as L import Language.REST.Types () -- Hashable (M.Map a b) +import Language.REST.Internal.Orphans () import Text.Printf -newtype PartialOrder a = PartialOrder (M.Map a (S.Set a)) +-- | Irreflexive (strict) partial orders +newtype PartialOrder a = + -- | @PartialOrder m@ represents the relation + -- + -- > (>) = { (a, b) | (a, bs) <- toList m, b <- bs } + -- + -- Transitivity implies that @m ! a == { b | a > b}@ if @a@ is in the map. + -- + -- Asymmetry implies that @member a (m ! b)@ implies + -- @not (member b (m ! a))@. + -- + -- Irreflexivity means that @a@ cannot be in @m ! a@. + -- + PartialOrder (M.Map a (S.Set a)) deriving (Ord, Eq, Generic, Hashable) instance (Show a) => Show (PartialOrder a) where @@ -40,21 +54,27 @@ isEmpty :: Eq a => PartialOrder a -> Bool isEmpty p = p == empty +-- | @canInsert (>) a b@ iff @a /= b && not (a > b) && not (b > a)@ canInsert :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Bool canInsert o f g = f /= g && not (gt o f g) && not (gt o g f) +-- | @gt (>) a b == (a > b)@ gt :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Bool gt po t u = S.member u $ descendents t po unionDisjointUnsafe :: Ord a => PartialOrder a -> PartialOrder a -> PartialOrder a unionDisjointUnsafe (PartialOrder m) (PartialOrder m') = PartialOrder (M.union m m') +-- | ascendants a (>) = { b | b > a } ascendants :: Ord k => k -> PartialOrder k -> S.Set k ascendants k (PartialOrder m) = M.keysSet $ M.filter (S.member k) m +-- | descendents a (>) = { b | a > b } descendents :: Ord a => a -> PartialOrder a -> S.Set a descendents k (PartialOrder m) = M.findWithDefault S.empty k m +-- | @insertUnsafe (>) a b@ is unsafe because it may not respect some +-- of its properties if @canInsert (>) a b@ doesn't hold. {-# INLINE insertUnsafe #-} insertUnsafe :: Ord a => PartialOrder a -> a -> a -> PartialOrder a insertUnsafe o@(PartialOrder m) f g = result @@ -83,6 +103,21 @@ elems :: (Eq a, Ord a, Hashable a) => PartialOrder a -> S.Set a elems (PartialOrder m) = S.union (M.keysSet m) (S.unions (M.elems m)) +-- | @replaceUnsafe olds new (>)@ replaces every element in @olds@ with +-- @new@ in the partial order @(>)@. +-- +-- More formally: +-- +-- > replaceUnsafe olds new (>) = +-- > { (a, b) | notElem a olds, notElem b olds } +-- > U { (new, b) | o <- olds, o > b } +-- > U { (a, new) | o <- olds, a > o } +-- +-- This operation is unsafe because it only yields a partial order +-- if forall @o@ in @olds@: +-- * @o > b@ implies @not (b > new)@, and +-- * @a > o@ implies @not (new > a)@. +-- replaceUnsafe :: (Eq a, Ord a, Hashable a) => [a] -> a -> PartialOrder a -> PartialOrder a replaceUnsafe froms to po@(PartialOrder m) = result where diff --git a/src/Language/REST/Internal/WQO.hs b/src/Language/REST/Internal/WQO.hs --- a/src/Language/REST/Internal/WQO.hs +++ b/src/Language/REST/Internal/WQO.hs @@ -35,6 +35,7 @@ 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 @@ -71,8 +72,13 @@ getECs :: WQO a -> S.Set (EquivalenceClass a) getECs (WQO ecs _) = ecs --- Invariant: the first set contains all ECs -data WQO a = WQO (S.Set (EquivalenceClass a)) (PartialOrder (EquivalenceClass a)) +-- | Well-founded reflexive partial orders +data WQO a = + -- Invariant: the first set contains all equivalence classes + -- + -- The strict partial order describes the ordering of the + -- equivalence classes in the first set. + WQO (S.Set (EquivalenceClass a)) (PartialOrder (EquivalenceClass a)) deriving (Ord, Eq, Generic, Hashable) instance (Show a, Eq a, Hashable a) => Show (WQO a) where @@ -100,6 +106,10 @@ elems :: (Ord a) => WQO a -> S.Set a elems (WQO ec _) = S.unions $ map EC.elems (S.toList ec) +-- | @getEquivalenceClasses (>=) a b@ retrieves the equivanlence classes of +-- @a@ and @b@. +-- +-- TODO: Why are these looked up in pairs and not individually? {-# INLINE getEquivalenceClasses #-} getEquivalenceClasses :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a -> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a)) @@ -109,6 +119,8 @@ u = L.find (EC.isMember target) classes' classes' = S.toList classes +-- | Like @getEquivalenceClasses@ but only yields a result +-- if classes of equivalence are found for both elements. {-# INLINE getEquivalenceClasses' #-} getEquivalenceClasses' :: (Ord a, Hashable a) @@ -125,6 +137,8 @@ where classes' = S.toList classes +-- | @getRelation (>=) a b == QEQ@ iff @a >= b@ +-- @getRelation (>=) a b == QGT@ iff @a > b@ {-# INLINE getRelation #-} getRelation :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a -> Maybe QORelation getRelation _ f g | f == g = Just QEQ @@ -138,6 +152,8 @@ else Nothing | otherwise = Nothing +-- | @expandEC (>=) ec x@ adds an element @x@ to the equivalence class +-- @ec@ of @(>=)@. expandEC :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> a -> WQO a expandEC (WQO ecs po) ec x = WQO ecs' po' where @@ -145,6 +161,8 @@ ecs' = S.insert ec' $ S.delete ec ecs po' = PO.replaceUnsafe [ec] ec' po +-- | @mergeECs (>=) ec1 ec2@ combines the equivalence classes @ec1@ and @ec2@ +-- of @(>=)@. mergeECs :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> EquivalenceClass a -> WQO a mergeECs (WQO ecs po) ec1 ec2 = WQO ecs' po' where @@ -311,7 +329,7 @@ (Just ec1, Just ec2) -> WQO ecs (PO.insertUnsafe po ec1 ec2) - +-- | Generates all the possible orderings of the elements in the given set. orderings :: forall a. (Ord a, Eq a, Hashable a) => S.Set a -> S.Set (WQO a) orderings ops = go S.empty (S.singleton empty) where diff --git a/src/Language/REST/Internal/WorkStrategy.hs b/src/Language/REST/Internal/WorkStrategy.hs --- a/src/Language/REST/Internal/WorkStrategy.hs +++ b/src/Language/REST/Internal/WorkStrategy.hs @@ -9,30 +9,30 @@ 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 diff --git a/src/Language/REST/Op.hs b/src/Language/REST/Op.hs --- a/src/Language/REST/Op.hs +++ b/src/Language/REST/Op.hs @@ -37,4 +37,6 @@ go ' ' = "_space_" go '∪' = "_cup_" go '\\' = "_bslash_" + go '(' = "_lp_" + go ')' = "_rp_" go c = singleton c diff --git a/src/Language/REST/RESTDot.hs b/src/Language/REST/RESTDot.hs --- a/src/Language/REST/RESTDot.hs +++ b/src/Language/REST/RESTDot.hs @@ -11,11 +11,15 @@ import Language.REST.Dot import Language.REST.Path +data ShowRejectsOpt = + ShowRejectsWithRule | ShowRejectsWithoutRule | HideRejects + deriving Eq + data PrettyPrinter rule term ord = PrettyPrinter { printRule :: rule -> String , printTerm :: term -> String , printOrd :: ord -> String - , showRejects :: Bool + , showRejects :: ShowRejectsOpt } rejNodeID :: (Hashable rule, Hashable term, Hashable a) => GraphType -> Path rule term a -> term -> String @@ -23,7 +27,7 @@ rejectedNodes :: forall rule term a . (Hashable rule, Hashable term, Hashable a) => GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Node -rejectedNodes _ pp _ | not (showRejects pp) = S.empty +rejectedNodes _ pp _ | showRejects pp == HideRejects = S.empty rejectedNodes gt pp p@(_steps, (PathTerm {rejected})) = S.fromList $ map go (HS.toList rejected) where go :: (term, rule) -> Node @@ -55,12 +59,16 @@ rejEdges :: Path rule term a -> S.Set Edge rejEdges p@(_, PathTerm _ rej) = - if showRejects pp + if showRejects pp /= HideRejects then S.fromList $ map go (HS.toList rej) else S.empty where + ruleText r = + if showRejects pp == ShowRejectsWithRule + then printRule pp r + else "" go (rejTerm, r) = - Edge (nodeID (endNode gt pp p)) (rejNodeID gt p rejTerm) (printRule pp r) "red" " " "dotted" + Edge (nodeID (endNode gt pp p)) (rejNodeID gt p rejTerm) (ruleText r) "red" " " "dotted" toEdge :: (Path rule term a, Path rule term a) -> Edge diff --git a/src/Language/REST/Rest.hs b/src/Language/REST/Rest.hs --- a/src/Language/REST/Rest.hs +++ b/src/Language/REST/Rest.hs @@ -57,51 +57,47 @@ 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' (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 @@ , 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 @@ (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) diff --git a/src/Language/REST/Types.hs b/src/Language/REST/Types.hs --- a/src/Language/REST/Types.hs +++ b/src/Language/REST/Types.hs @@ -6,8 +6,8 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} -{-# OPTIONS_GHC -Wno-orphans #-} + module Language.REST.Types ( prettyPrint , PPArgs(..) @@ -22,7 +22,6 @@ import qualified Data.List as L import qualified Data.HashSet as S import qualified Data.Set as OS -import qualified Data.Map as M import qualified Data.Text as T import Text.Printf @@ -69,11 +68,6 @@ show GTE = "≥" show EQ = "≅" -instance Hashable a => Hashable (OS.Set a) where - hashWithSalt i s = hashWithSalt i (OS.toList s) - -instance (Hashable a, Hashable b) => Hashable (M.Map a b) where - hashWithSalt i s = hashWithSalt i (M.toList s) toOrderedSet :: (Eq a, Hashable a, Ord a) => S.HashSet a -> OS.Set a toOrderedSet = OS.fromList . S.toList diff --git a/test/BagExample.hs b/test/BagExample.hs --- a/test/BagExample.hs +++ b/test/BagExample.hs @@ -105,14 +105,13 @@ RESTParams { re = S.empty , ru = rules - , toET = id , target = Nothing , workStrategy = bfs , ocImpl = impl , initRes = pathsResult , etStrategy = ExploreWhenNeeded } (bag start) - let prettyPrinter = PrettyPrinter showRule showBag show True + let prettyPrinter = PrettyPrinter showRule showBag show ShowRejectsWithRule writeDot "example" Tree prettyPrinter (toOrderedSet paths) where impl = lift SC.strictOC $ cmapConstraints toMultiset (multisetOrder compareChar) diff --git a/test/ExploredTerms.hs b/test/ExploredTerms.hs new file mode 100644 --- /dev/null +++ b/test/ExploredTerms.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} + +module ExploredTerms where + +import Control.Monad.Identity +import Data.Hashable +import qualified Data.HashSet as S +import GHC.Generics (Generic) + +import Language.REST.ExploredTerms as ET + +type Constraints = Int + +-- 2nd argument is cost to explore +data Term = Term String Int + deriving (Eq, Generic, Hashable, Show) + +exploreFuncs :: ExploreFuncs Term Constraints Identity +exploreFuncs = EF undefined subsume refine where + subsume c0 c1 = return $ c0 >= c1 + refine c _ (Term _ dest) = c - dest + +t0 :: Term +t0 = Term "t0" 5 + +t1 :: Term +t1 = Term "t1" 0 + +t2 :: Term +t2 = Term "t2" 0 + +et0 :: ExploredTerms Term Constraints Identity +et0 = ET.empty exploreFuncs ExploreWhenNeeded + +et :: ExploredTerms Term Constraints Identity +et = ET.insert t1 15 (S.fromList [t0]) $ ET.insert t0 14 (S.fromList [t2]) et0 + +tests :: [(String, Bool)] +tests = + [ -- Described in https://github.com/zgrannan/rest/issues/9 + ("Explore-opt", not $ runIdentity $ shouldExplore t1 17 et) + + , ("Explore", runIdentity $ shouldExplore t1 21 et) + ] diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -8,6 +8,7 @@ import Control.Monad.Identity import Data.Time.Clock import Data.Hashable +import qualified Data.Set as DS import qualified Data.HashSet as S import Text.Printf @@ -25,6 +26,7 @@ import qualified Lists as Li import Language.REST.Core +import Language.REST.ConcreteOC import Language.REST.ExploredTerms import Language.REST.OCAlgebra import Language.REST.OCToAbstract @@ -84,12 +86,12 @@ { gShowConstraints :: Bool , gTarget :: Maybe String , gGraphType :: GraphType - , gShowRejects :: Bool + , gShowRejects :: ShowRejectsOpt , gUseETOpt :: Bool } defaultParams :: GraphParams -defaultParams = GraphParams False Nothing Tree True True +defaultParams = GraphParams False Nothing Tree ShowRejectsWithoutRule True withTarget :: String -> GraphParams -> GraphParams withTarget target0 gp = gp{gTarget = Just target0} @@ -101,10 +103,13 @@ withNoETOpt gp = gp{gUseETOpt = False} withHideRejects :: GraphParams -> GraphParams -withHideRejects gp = gp{gShowRejects = False} +withHideRejects gp = gp{gShowRejects = HideRejects} -data SolverType = LPOStrict | LPO | RPO | KBO | Fuel Int +withShowRejectsRule :: GraphParams -> GraphParams +withShowRejectsRule gp = gp{gShowRejects = ShowRejectsWithRule} +data SolverType = LPOStrict | LPO | RPO | RPOConcrete [Op] | KBO | Fuel Int + mkRESTGraph :: SolverType -> S.HashSet Rewrite @@ -119,6 +124,8 @@ withZ3 $ \z3 -> mkRESTGraph' (lift (AC.adtOC z3) lpo) evalRWs0 userRWs0 name term0 params mkRESTGraph RPO evalRWs0 userRWs0 name term0 params = withZ3 $ \z3 -> mkRESTGraph' (lift (AC.adtOC z3) rpo) evalRWs0 userRWs0 name term0 params +mkRESTGraph (RPOConcrete ops) evalRWs0 userRWs0 name term0 params = + mkRESTGraph' (concreteOC $ DS.fromList ops) evalRWs0 userRWs0 name term0 params mkRESTGraph KBO evalRWs0 userRWs0 name term0 params = withZ3 $ \z3 -> mkRESTGraph' (kbo z3) evalRWs0 userRWs0 name term0 params mkRESTGraph (Fuel n) evalRWs0 userRWs0 name term0 params = @@ -142,7 +149,6 @@ RESTParams { re = evalRWs0 , ru = userRWs0 - , toET = id , target = fmap parseTerm (gTarget params) , workStrategy = bfs , ocImpl = impl @@ -162,16 +168,20 @@ Nothing -> printf "TARGET %s NOT FOUND\n" (pp (parseTerm target1))) Nothing -> return () +setDistribRules :: S.HashSet Rewrite +setDistribRules = S.fromList + [ distribL (/\) (\/) + , distribR (/\) (\/) + , distribL (\/) (/\) + , distribR (\/) (/\) + ] + challengeRulesNoCommute :: S.HashSet Rewrite -challengeRulesNoCommute = S.fromList +challengeRulesNoCommute = S.union setDistribRules $ S.fromList [ x /\ x ~> x , x \/ x ~> x , x \/ emptyset ~> x , x /\ emptyset ~> emptyset - , distribL (/\) (\/) - , distribR (/\) (\/) - , distribL (\/) (/\) - , distribR (\/) (/\) , assocL (\/) , assocR (\/) ] diff --git a/test/Test.hs b/test/Test.hs --- a/test/Test.hs +++ b/test/Test.hs @@ -12,6 +12,7 @@ import qualified Arith as A import qualified Data.HashMap.Strict as M +import qualified ExploredTerms as ExploredTerms import OpOrdering import DSL import WQO as WQO @@ -56,7 +57,6 @@ RESTParams { re = evalRWs , ru = userRWs - , toET = id , target = Nothing , workStrategy = notVisitedFirst , ocImpl = ?impl @@ -131,7 +131,7 @@ )) , ("Eval1", arithEQ (intToTerm 2 .+ intToTerm 3) 5) , ("Eval2", arithEQ (ack (intToTerm 3) (intToTerm 2)) 29) - , ("Subst1", return $ subst (M.fromList [("x", intToTerm 1), ("y", intToTerm 2)]) (x #+ y) == (intToTerm 1 .+ intToTerm 2)) + , ("Subst1", return $ subst (M.fromList [("X", intToTerm 1), ("Y", intToTerm 2)]) (x #+ y) == (intToTerm 1 .+ intToTerm 2)) , ("ArithTerm", termTest) , ("ArithTerm2", termTest2) , ("Arith0", eq (t1 .+ t2 .+ intToTerm 1) (t1 .+ (intToTerm 1 .+ t2))) @@ -237,6 +237,7 @@ go z3 = do putStrLn "Running REST Test Suite" + runTestSuite "ExploredTerms" ExploredTerms.tests runTestSuite "SMT" SMT.tests runTestSuite "KBO" (KBO.tests z3) _ <- QuickCheckTests.tests diff --git a/testlib/DSL.hs b/testlib/DSL.hs --- a/testlib/DSL.hs +++ b/testlib/DSL.hs @@ -33,11 +33,11 @@ d = App (Op "d") [] x, y, v, w, z' :: MT.MetaTerm -x = MT.Var "x" -y = MT.Var "y" -v = MT.Var "v" -w = MT.Var "w" -z' = MT.Var "z" +x = MT.Var "X" +y = MT.Var "Y" +v = MT.Var "V" +w = MT.Var "W" +z' = MT.Var "Z" f, g, h :: Op f = Op "f" diff --git a/testlib/Language/REST/ConcreteOC.hs b/testlib/Language/REST/ConcreteOC.hs --- a/testlib/Language/REST/ConcreteOC.hs +++ b/testlib/Language/REST/ConcreteOC.hs @@ -7,53 +7,26 @@ import qualified Language.REST.Internal.WQO as WQO import Language.REST.RuntimeTerm import Language.REST.RPO -import Language.REST.Internal.OpOrdering -import Language.REST.MetaTerm +import Language.REST.Op -import Data.List as L import Data.Hashable import GHC.Generics (Generic) import qualified Data.Set as S -data ConcreteOC = ConcreteOC [RuntimeTerm] (Maybe OpOrdering) +data ConcreteOC = ConcreteOC (S.Set (WQO.WQO Op)) deriving (Eq, Ord, Generic, Hashable) instance Show ConcreteOC where - show (ConcreteOC _ (Just oo)) = show oo - show _ = "impossible" - -isSat :: ConcreteOC -> Bool -isSat (ConcreteOC _ (Just _)) = True -isSat _ = False - -getOrdering :: [RuntimeTerm] -> Maybe OpOrdering -getOrdering ts = - let - ops = S.unions $ map termOps ts - orderings = S.toList $ WQO.orderings ops - in - L.find (`orients` ts) orderings + show (ConcreteOC ords) = show (S.size ords) ++ " orderings" +concreteOC :: Monad m => S.Set Op -> AOC.OCAlgebra ConcreteOC RuntimeTerm m +concreteOC ops = AOC.OCAlgebra (return . isSat) refine (ConcreteOC (WQO.orderings ops)) union notStrongerThan + where + union (ConcreteOC ord1) (ConcreteOC ord2) = ConcreteOC $ S.union ord1 ord2 + notStrongerThan (ConcreteOC ord1) (ConcreteOC ord2) = return $ ord1 == ord2 || ord2 `S.isSubsetOf` ord1 -orients :: OpOrdering -> [RuntimeTerm] -> Bool -orients ordering terms = - let - pairs = zip terms (tail terms) - in - all (uncurry $ synGTE ordering) pairs + isSat :: ConcreteOC -> Bool + isSat (ConcreteOC ords) = not $ S.null ords -concreteOC :: Monad m => AOC.OCAlgebra ConcreteOC RuntimeTerm m -concreteOC = AOC.OCAlgebra (return . isSat) refine (ConcreteOC [] (Just (WQO.empty))) constUnion notStrongerThan - where - constUnion t1 _ = t1 - notStrongerThan _ _ = return False refine :: ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC - refine (ConcreteOC ts (Just o)) _ u = - let - ts' = ts ++ [u] - in - ConcreteOC ts' $ - if o `orients` ts' - then Just o - else getOrdering ts' - refine (ConcreteOC ts Nothing) _ u = ConcreteOC (ts ++ [u]) Nothing + refine (ConcreteOC ords) t u = ConcreteOC (S.filter (\ord -> synGTE ord t u) ords)