packages feed

rest-rewrite 0.2.0 → 0.3.0

raw patch · 17 files changed

+276/−144 lines, 17 filesdep ~hashable

Dependency ranges changed: hashable

Files

rest-rewrite.cabal view
@@ -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 <zgrannan@cs.ubc.ca> author:             Zack Grannan <zgrannan@cs.ubc.ca> 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
src/Language/REST/ExploredTerms.hs view
@@ -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
src/Language/REST/Internal/EquivalenceClass.hs view
@@ -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
+ src/Language/REST/Internal/Orphans.hs view
@@ -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
src/Language/REST/Internal/PartialOrder.hs view
@@ -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
src/Language/REST/Internal/WQO.hs view
@@ -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
src/Language/REST/Internal/WorkStrategy.hs view
@@ -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
src/Language/REST/Op.hs view
@@ -37,4 +37,6 @@         go ' '  = "_space_"         go '∪'  = "_cup_"         go '\\' = "_bslash_"+        go '(' = "_lp_"+        go ')' = "_rp_"         go c    = singleton c
src/Language/REST/RESTDot.hs view
@@ -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
src/Language/REST/Rest.hs view
@@ -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)
src/Language/REST/Types.hs view
@@ -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
test/BagExample.hs view
@@ -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)
+ test/ExploredTerms.hs view
@@ -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)+  ]
test/Main.hs view
@@ -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 (\/)   ]
test/Test.hs view
@@ -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
testlib/DSL.hs view
@@ -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"
testlib/Language/REST/ConcreteOC.hs view
@@ -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)