rest-rewrite 0.3.0 → 0.4.0

raw patch · 32 files changed

+470/−320 lines, 32 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• rest-rewrite.cabal +2/−1
• src/Language/REST.hs +2/−33
• src/Language/REST/Core.hs +9/−51
• src/Language/REST/Dot.hs +26/−5
• src/Language/REST/ExploredTerms.hs +25/−5
• src/Language/REST/Internal/ListT.hs +44/−0
• src/Language/REST/Internal/MultiSet.hs +7/−0
• src/Language/REST/Internal/MultisetOrder.hs +8/−1
• src/Language/REST/Internal/OpOrdering.hs +12/−15
• src/Language/REST/Internal/Rewrite.hs +20/−4
• src/Language/REST/Internal/Util.hs +4/−0
• src/Language/REST/Internal/WQO.hs +5/−0
• src/Language/REST/Internal/WorkStrategy.hs +11/−11
• src/Language/REST/KBO.hs +4/−0
• src/Language/REST/LPO.hs +3/−0
• src/Language/REST/MetaTerm.hs +2/−7
• src/Language/REST/OCAlgebra.hs +23/−15
• src/Language/REST/OCToAbstract.hs +3/−3
• src/Language/REST/Op.hs +1/−0
• src/Language/REST/Path.hs +14/−6
• src/Language/REST/RESTDot.hs +14/−2
• src/Language/REST/RPO.hs +9/−1
• src/Language/REST/Rest.hs +19/−6
• src/Language/REST/RewriteRule.hs +5/−0
• src/Language/REST/RuntimeTerm.hs +20/−1
• src/Language/REST/SMT.hs +50/−14
• src/Language/REST/Types.hs +12/−1
• src/Language/REST/WQOConstraints.hs +42/−22
• src/Language/REST/WQOConstraints/ADT.hs +16/−54
• src/Language/REST/WQOConstraints/Lazy.hs +14/−24
• src/Language/REST/WQOConstraints/Strict.hs +26/−37
• test/Test.hs +18/−1

@@ -1,6 +1,6 @@ name:               rest-rewrite build-type:         Simple-version:            0.3.0+version:            0.4.0 cabal-version:      2.0 category:           Rewriting maintainer:         Zack Grannan <zgrannan@cs.ubc.ca>@@ -22,6 +22,7 @@     Language.REST.Dot     Language.REST.ExploredTerms     Language.REST.Internal.EquivalenceClass+    Language.REST.Internal.ListT     Language.REST.Internal.MultiSet     Language.REST.Internal.MultisetOrder     Language.REST.Internal.OpOrdering

@@ -2,47 +2,16 @@  module Language.REST where -import Control.Monad.Identity-import Data.Hashable-import Data.Maybe-import qualified Data.HashSet as S- import Language.REST.OCAlgebra (OCAlgebra) import Language.REST.OCToAbstract-import Language.REST.WQOConstraints import Language.REST.WQOConstraints.ADT (ConstraintsADT, adtOC) import Language.REST.RPO import Language.REST.RuntimeTerm import Language.REST.Op-import Language.REST.Internal.OpOrdering-import qualified Language.REST.Internal.WQO as WQO import System.IO (Handle)  +-- | 'adtRPO' Is an ordering constraint algebra derived from the recursive+-- path ordering; it is a useful general-purpose OCA. adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO adtRPO z3 = lift (adtOC z3) rpo--- lazyRPO = lift lazyOC rpo--- strictRPO = lift strictOC rpo---- Assume vars are arity 0, which is usually correct-getVars :: RuntimeTerm -> S.HashSet Op-getVars (App op []) = S.singleton op-getVars (App _op xs) = S.unions (map getVars xs)---varsEQ :: RuntimeTerm -> RuntimeTerm -> WQO.WQO Op-varsEQ t1 t2 =-  let-    vars = getVars t1 `S.union` getVars t2-  in-    fromJust $ WQO.mergeAll (map (uncurry (=.)) (pairs (S.toList vars)))-  where-    pairs xs | length xs < 2 = []-    pairs xs | otherwise = zip xs (tail xs)--cgen :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity-cgen impl r oc t1 t2 =-  let-    Identity rpoc = rpo impl r oc t1 t2-  in-    return $ addConstraint impl (varsEQ t1 t2) rpoc

@@ -1,59 +1,17 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE ImplicitParams #-} +-- | Core REST functions module Language.REST.Core where -import Prelude hiding (GT, EQ)--import           Debug.Trace                    ( trace )-import qualified Data.List                     as L-import qualified Data.HashSet                      as S- import           Language.REST.OCAlgebra-import           Language.REST.Types-import qualified Language.REST.MetaTerm as MT-import           Language.REST.Internal.Rewrite-import           Language.REST.RuntimeTerm as RT-import           Language.REST.RewriteRule--type MetaTerm = MT.MetaTerm---contains :: RuntimeTerm -> RuntimeTerm -> Bool-contains t1 t2 | t1 == t2 = True-contains (App _ ts) t     = any (contains t) ts---orient' :: Show oc => (?impl :: OCAlgebra oc RuntimeTerm m) => oc -> [RuntimeTerm] -> oc-orient' oc0 ts0 = go oc0 (zip ts0 (tail ts0))-  where-    go oc []            = oc-    go oc ((t0, t1):ts) = go (refine ?impl oc t0 t1) ts+import           Language.REST.RuntimeTerm -orient :: Show oc =>  OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc-orient impl = orient' (top impl)+-- | @orient impl ts@ generates the constraints on an ordering defined by the+--   OCA `impl`, that ensures each term in the path `ts` is smaller than or+--   equal to the previous one.+orient :: OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc+orient impl ts0 = go (top impl) (zip ts0 (tail ts0))    where-     ?impl = impl--canOrient :: forall oc m . Show oc-  => (?impl :: OCAlgebra oc RuntimeTerm m) => [RuntimeTerm] -> m Bool-canOrient terms = trace ("Try to orient " ++ termPathStr terms) $ isSat ?impl (orient ?impl terms)--syms :: MetaTerm -> S.HashSet String-syms (MT.Var s)      = S.singleton s-syms (MT.RWApp _ xs) = S.unions (map syms xs)--termPathStr :: [RuntimeTerm] -> String-termPathStr terms = L.intercalate " --> \n" (map pp terms)-  where-    pp = prettyPrint (PPArgs [] [] (const Nothing))--eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm-eval rws t0 =-  do-    result <- mapM (apply t0) (S.toList rws)-    case S.toList $ S.unions result of-      []      -> return t0-      (t : _) -> eval rws t+    go oc []            = oc+    go oc ((t0, t1):ts) = go (refine impl oc t0 t1) ts

@@ -2,7 +2,15 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE ScopedTypeVariables #-} -module Language.REST.Dot where+-- | This module contains functionality for generating GraphViz graphs+module Language.REST.Dot+  ( mkGraph+  , DiGraph(..)+  , Edge(..)+  , GraphType(..)+  , Node(..)+  , NodeID+  ) where  import GHC.Generics import Data.Hashable@@ -11,12 +19,24 @@ import Text.Printf import System.Process -data DiGraph = DiGraph String (S.Set Node) (S.Set Edge);+-- | A GraphViz directed graph+data DiGraph = DiGraph+  String -- ^ Filename+  (S.Set Node)+  (S.Set Edge);  type NodeID =  String -data GraphType = Tree | Dag | Min deriving (Read)+-- | The way the graph will be rendered+data GraphType =+    Tree -- ^ Standard representation+  | Dag  -- ^ In 'Dag', If two equal terms `n` steps from the root are the same, they are+         --   represented by the same node, even if they were reached via different+         --   paths+  | Min  -- ^ Each unique term is represented by the same node+  deriving (Read) +-- | A GraphViz node data Node = Node      { nodeID     :: NodeID     , label      :: String@@ -24,6 +44,7 @@     , labelColor :: String     } deriving (Eq, Ord, Show, Generic, Hashable) +-- A GraphViz edge data Edge = Edge     { from      :: NodeID     , to        :: NodeID@@ -33,8 +54,6 @@     , edgeStyle :: String     } deriving (Eq, Ord, Show, Generic, Hashable) -type DotPath = [Node]- nodeString :: Node -> String nodeString (Node nid elabel style color) =     printf "\t%s [label=\"%s\"\nstyle=\"%s\"\ncolor=\"%s\"];" nid elabel style color@@ -68,6 +87,8 @@         edgesString = intercalate "\n" (map edgeString (S.toList edges))  +-- | @mkGraph name graph@ generates the @.dot@ file for @graph@, and renders+--   the resulting graph to a @png@ file using the @dot@ utility mkGraph :: String -> DiGraph -> IO () mkGraph name graph = do   let dotfile = printf "graphs/%s.dot" name

@@ -21,18 +21,34 @@  import Prelude hiding (lookup) +-- | 'ExploreStrategy' defines how 'shouldExplore' should decide whether or not+-- | to consider rewrites from a given term data ExploreStrategy =-  ExploreAlways | ExploreLessConstrained | ExploreWhenNeeded | ExploreOnce+    ExploreAlways -- ^ Always explore, even when it's not necessary.+  | ExploreLessConstrained -- ^ Explore terms unless the constraints are stricter.+                           -- This may stil explore unnecessary paths, the terms+                           -- were already fully explored with the different constraints.+  | ExploreWhenNeeded -- ^ Explore terms unless the constraints are stricter OR if all+                      --   terms reachable via transitive rewrites were already explored.+  | ExploreOnce -- ^ Explore each term only once. This may cause some terms not to be+                --   explored if the terms leading to them were initially visited at+                --   strict constraints. + data ExploreFuncs term c m = EF-  { union           :: c -> c -> c+  { -- | When a term @t@ is visited at constraints @c0@, and then at constraints+    --   @c1@, the constraints for term @t@ is set to @c0 `union` c1@+    union           :: c -> c -> c     -- | @c0 `subsumes` c1@ if @c0@ permits all orderings permited by @c1@   , subsumes        :: c -> c -> m Bool+    -- | @'exRefine' c t u@ strengthens constraints @c@ to permit the rewrite step+    --   from @t@ to @u@. This is used to determine if considering term @u@ by rewriting+    --   from @t@ would permit more rewrite applications.   , 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+-- | 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 term c m) ExploreStrategy @@ -54,7 +70,8 @@ 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.+-- defined as in the REST paper. Also incorporates an optimization described+-- here: https://github.com/zgrannan/rest/issues/9 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,exRefine}) _) = result where@@ -89,6 +106,9 @@   -- There exists a reachable term that has never previously been seen; not fully explored   go _ _        | otherwise = return False +-- | @'shouldExplore' t c et@ determines if rewrites originating from term @t@ at+--   constraints @c@ should be considered, given the already explored terms of @et@+--   and the associated 'ExploreStrategy' 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) =

@@ -0,0 +1,44 @@+-- | Defines a version of the ListT monad transformer, used in the REST search++module Language.REST.Internal.ListT where++import           Control.Applicative+import           Control.Monad.Trans++data ListT m a = ListT {+  runListT :: m [a]+}++instance (Monad m) => Functor (ListT m) where+  fmap f (ListT mxs) = ListT $ do+    xs <- mxs+    return $ map f xs++instance (Monad m) => Applicative (ListT m) where+  pure x                    = ListT (return [x])+  (ListT mf) <*> (ListT mx) = ListT $ do+    fs <- mf+    xs <- mx+    return $ do+      f <- fs+      map f xs++instance (Monad m) => Monad (ListT m) where+  return x         = ListT (return [x])+  (ListT mxs) >>= f = ListT $ do+    xs <- mxs+    res <- mapM (runListT . f) xs+    return $ concat res++instance (Monad m) => Alternative (ListT m) where+  empty                       = ListT (return [])+  (ListT mxs) <|> (ListT mys) = ListT $ do+    xs <- mxs+    if not $ null xs+      then mxs+      else mys++instance MonadTrans ListT where+  lift mx = ListT $ do+    x <- mx+    return [x]

@@ -31,9 +31,14 @@ instance Show a => Show (MultiSet a) where   show ms = "{" ++ L.intercalate ", " (map show $ toList ms) ++ "}" +-- | @delete k m@ removes a single instance of @k@ from the multiset @m.+--   If @k is not in the multiset, the original multiset is returned delete :: (Hashable a, Eq a) => a -> MultiSet a -> MultiSet a delete k = deleteMany k 1 +-- | @delete k n m@ removes @n@ instances of @k@ from the multiset @m@.+--   If there are less than @n@ instances of @k@ in the multiset, all+--   instances are removed. deleteMany :: (Hashable a, Eq a) => a -> Int -> MultiSet a -> MultiSet a deleteMany k v (MultiSet ms) | Just c <- M.lookup k ms                              , c > v = MultiSet $ M.insert k (c - v) ms@@ -56,6 +61,8 @@ null :: MultiSet a -> Bool null (MultiSet ms) = M.null ms +-- | @member k m@ returns @true@ iff there is at least one instance of @k@+--   in @m@ member :: (Eq a, Hashable a) => a -> MultiSet a -> Bool member k (MultiSet ms) = M.member k ms 

@@ -3,7 +3,10 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} -module Language.REST.Internal.MultisetOrder (multisetOrder, possibilities) where+-- | This module defines a constraint generator for a multiset+--   quasi-ordering. For more details, please see the definition+--   of @mul@ in section 4.2.1 of the paper.+module Language.REST.Internal.MultisetOrder (multisetOrder) where  import GHC.Generics import qualified Data.List as L@@ -49,6 +52,10 @@       (possibilities GTE xs (filter (not . flip elem ys') ys))  +-- | Given a [constraint generator]("Language.REST.WQOConstraints#t:ConstraintGen") @cgen@ that generates constraints a WQO on+--   @base@ implied by a relation between elements of @lifted@, @'multisetOrder' cgen@+--   yields a constraint generator on elements of base implied by a relation between+--   multisets of @lifted@. multisetOrder :: forall oc base lifted m . (Ord lifted, Ord base, Show base, Eq base, Hashable base, Hashable lifted, Eq lifted, Show (oc base), Eq (oc base),  Monad m) =>      ConstraintGen oc base lifted m   -> ConstraintGen oc base (MultiSet lifted) m

@@ -3,12 +3,11 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} -+-- | This module defines an interface for 'WQO's on 'Op'erators,+--   for example, that are used as the precedence for an [RPQO]("Language.REST.RPO"). module Language.REST.Internal.OpOrdering (     empty-  , merge   , OpOrdering-  , opInsert   , opGT   , opEQ   , (=.)@@ -31,33 +30,31 @@ type OpOrdering   = WQO Op  +-- | @opGT o f g@ returns @true@ if @f > g@ in @o@ opGT :: OpOrdering -> Op -> Op -> Bool opGT s f g = getRelation s f g == Just QGT +-- | @opEQ o f g@ returns @true@ if @f = g@ in @o@ opEQ :: OpOrdering -> Op -> Op -> Bool opEQ s f g = getRelation s f g == Just QEQ --opInsert :: OpOrdering -> Op -> Op -> QORelation -> Maybe OpOrdering-opInsert o f g r =-  case WQO.insert o (f, g, r) of-    ValidExtension o' -> Just o'-    _                 -> Nothing---- The following only are valid if f /= g.---- precondition : f /= g+-- |  @f >. g@ generates a new ordering with @f@ greater than @g@.+--   This function is undefined if f == g. (>.) :: Op -> Op -> OpOrdering (>.) f g = fromJust $ WQO.singleton (f, g, QGT) --- precondition : f /= g+-- |  @f =. g@ generates a new ordering with @f@ equal to @g@.+--   This function is undefined if f == g. (=.) :: Op -> Op -> OpOrdering (=.) f g = fromJust $ WQO.singleton (f, g, QEQ) --- precondition : f /= g+-- |  @f <. g@ generates a new ordering with @f@ less than @g@.+--   This function is undefined if f == g. (<.) :: Op -> Op -> OpOrdering (<.) f g = g >. f +-- | @parseOO str@ returns the ordering defined by @str@. If the input describes+--   /any/ ordering, (i.e "f = f"), then this function returns 'Nothing'. parseOO :: String -> Maybe OpOrdering parseOO str =   case parse parser "" str of

@@ -3,7 +3,13 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} -module Language.REST.Internal.Rewrite where+module Language.REST.Internal.Rewrite+  ( Rewrite(..)+  , Subst+  , named+  , subst+  , unify+  ) where  import GHC.Generics (Generic) @@ -17,17 +23,24 @@ import Language.REST.RuntimeTerm  +-- | @Rewrite t u s@ defines a rewrite rule \( t \rightarrow u \), with+--   an optional name @s@. data Rewrite = Rewrite MetaTerm MetaTerm (Maybe String)   deriving (Eq, Ord, Generic, Hashable, Show) +-- | 'Subst' is a mapping from variable names to 'RuntimeTerm's.+--   Normally this would be generated by unifying the left-hand-side of+--   a 'Rewrite' with a term. type Subst = M.HashMap String RuntimeTerm -getName :: Rewrite -> Maybe String-getName (Rewrite _t _u n) = n-+-- | @named r n@ assigns the name @n@ to rule @r@, replacing any+--   existing name named :: Rewrite -> String -> Rewrite named (Rewrite t u _) n = Rewrite t u (Just n) +-- | @subst s m@ replaces the variables in the 'MetaTerm' @m@ with 'RuntimeTerm's+--   in the substitution 's'. This function returns an error if any variables in 'm'+--   do not have a substituion subst :: Subst -> MetaTerm -> RuntimeTerm subst s (MT.Var v)  | Just t <- M.lookup v s = t                     | otherwise@@ -42,6 +55,9 @@   | otherwise   = Nothing +-- | @unify m r su@ extends the substitution @su@ to generate a new+--   substitution that unifies @m@ and @r@. Returns 'Nothing' if su+--   cannot be extended to unify the terms. unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst unify (MT.Var s) term su | M.lookup s su == Just term   = Just su

@@ -2,6 +2,10 @@  import qualified Data.List as L +-- | @removeEqBy f xs ys@ removes elements from @xs@ and @ys@ such that for each+--  element x removed from xs, an element y is removed from ys such @f x y@.+--  In other words in the result @(xs', ys')@, there does not exist any @x@ in+--  @xs'@, @y@ in @ys'@ such that @f x y@. removeEqBy :: (Eq a) => (a -> a -> Bool) -> [a] -> [a] -> ([a], [a]) removeEqBy _ [] ys = ([], ys) removeEqBy f (x : xs) ys

@@ -173,6 +173,8 @@ type ECMap a = M.Map (EquivalenceClass a) (EquivalenceClass a)  {-# SPECIALISE notStrongerThan :: WQO Op -> WQO Op -> Bool #-}+-- |  @w1 `notStrongerThan` w2@ if it is possible to extend @w1@ with additional+--    relations to obtain @w2@ notStrongerThan :: forall a . (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool notStrongerThan w1 w2 | w1 == w2 = True notStrongerThan (WQO ecs po) (WQO ecs' po') = result where@@ -251,6 +253,9 @@   | AlreadyImplied   | Contradicts +-- | @relevantTo wqo as bs@ returns a new WQO that contains only the necessary+--   relations to relate elements from @as@ with elements in @bs@ as they are+--   related in @wqo@. relevantTo :: (Ord a, Eq a, Hashable a) => WQO a -> S.Set a -> S.Set a -> WQO a relevantTo wqo0 as bs = go empty cartesianProduct where 

@@ -1,21 +1,30 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-module Language.REST.Internal.WorkStrategy where+module Language.REST.Internal.WorkStrategy (+  GetWork,+  WorkStrategy(..),+  bfs,+  notVisitedFirst) where  import Language.REST.ExploredTerms as ET import Language.REST.Path-import Language.REST.Internal.Rewrite  import Data.Hashable import qualified Data.List as L  type GetWork m rule term oc = [Path rule term oc] -> ExploredTerms term oc m -> (Path rule term oc, [Path rule term oc]) +-- | 'WorkStrategy' defines the procedure for choosing which pending path REST explores newtype WorkStrategy rule term oc = WorkStrategy (forall m . GetWork m rule term oc) +-- | Explore the rewrite tree in BFS style. Using this strategy enables finding the+--   shortest rewrite path to a desired term. bfs :: WorkStrategy rule term oc bfs = WorkStrategy bfs' +-- | Prioritize searching for terms that haven't been seen before. This strategy may+--   explore all reachable terms earlier, reducing the need to explore down the remaining+--   unexplored paths. notVisitedFirst :: (Eq term, Eq rule, Eq oc, Hashable term) => WorkStrategy rule term oc notVisitedFirst = WorkStrategy notVisitedFirst' @@ -28,12 +37,3 @@   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 . (Eq term, Eq oc, Hashable term) => WorkStrategy Rewrite term oc-commutesLast = WorkStrategy go where-  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-  fromComm (steps, _) = (getName . rule . last) steps == Just "mpComm"

@@ -25,6 +25,9 @@   toConstraint (sym, n) = toSMT sym `smtGTE` (Const n)  +-- | @kboGTE t u@ returns the SMT expression describing constraints+-- on the weights of function symbols such that @t@ is greater than @u@+-- in the KBO ordering. kboGTE :: RuntimeTerm -> RuntimeTerm -> SMTExpr Bool kboGTE t u = arityConstraints t `smtAnd` arityConstraints u `smtAnd` (size tOps `smtGTE` size uOps)   where@@ -32,6 +35,7 @@     size ops     = smtAdd (map toSMT ops)  +-- | OCA for a quasi-order extension to the Knuth-Bendix ordering kbo :: SolverHandle -> OCAlgebra (SMTExpr Bool) RuntimeTerm IO kbo solver = OCAlgebra   {  isSat           = checkSat' solver

@@ -82,8 +82,11 @@       go ui = lpo' strict oc GT cs t ui  +-- | Constraint generator for a quasi-order extension to the Lexicographic path ordering lpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity lpo oc r cs t u = return $ lpo' False oc r cs t u +-- | Constraint generator for a strict version of the quasi-order extension to+--   the Lexicographic path ordering. lpoStrict :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity lpoStrict oc r cs t u = return $ lpo' True oc r cs t u

@@ -6,11 +6,11 @@ import Data.String import Data.Hashable import GHC.Generics (Generic)-import qualified Data.Set as S  import Language.REST.Op import Language.REST.RuntimeTerm +-- | A MetaTerm is a term with variables; used for 'Rewrite' rules data MetaTerm =     Var String   | RWApp Op [MetaTerm] deriving (Eq, Ord, Show, Generic, Hashable)@@ -18,6 +18,7 @@ instance IsString MetaTerm where   fromString = Var +-- | Helper class, enabling conversion of 'RuntimeTerm's to 'MetaTerm's class ToMetaTerm a where   toMetaTerm :: a -> MetaTerm @@ -26,9 +27,3 @@  instance ToMetaTerm RuntimeTerm where   toMetaTerm (App f xs) = RWApp f (map toMetaTerm xs)--termOps :: ToMetaTerm a => a -> S.Set Op-termOps = go . toMetaTerm where-  go :: MetaTerm -> S.Set Op-  go (Var _)         = S.empty-  go (RWApp op trms) = S.insert op (S.unions (map go trms))

@@ -2,18 +2,22 @@ {-# LANGUAGE ScopedTypeVariables #-} module Language.REST.OCAlgebra where +-- | The "Ordering Constraint Algebra", as described in section 4.2 of the paper.+--  @OCAlgebra c a m@ is an OCA with language of constraints @c@, applied to terms+--  of type @a@. @m@ is the computation context for @isSat@. data OCAlgebra c a m = OCAlgebra-  {-    isSat  :: c -> m Bool-  , refine :: c -> a -> a -> c-  , top    :: c+  { isSat  :: c -> m Bool       -- ^ Checks if the constraints are satisfiable+  , refine :: c -> a -> a -> c  -- ^ @refine c t u@ strengthens @c@ to permit @t >= u@+  , top    :: c                 -- ^ Initial constraints for use in REST -  -- For explore optimizations, if not required just make it return 2nd param-  , union  :: c -> c -> c-  -- If not required return False-  , notStrongerThan :: c -> c -> m Bool+  , union  :: c -> c -> c       -- ^ Computes the union of constraints; used in 'ExploredTerms' as an optimization+                                --   A safe default implementation is @union c1 c2 = c2@++  , notStrongerThan :: c -> c -> m Bool -- ^ @c1 `notStrongerThan c2@ if @c1@ permits all orderings allowed by @c2@+                                        -- A safe default implementation is @notStrongerThan _ _ = return false@   } +-- | @fuelOC n@ is an OCA that permits @n@ rewrite steps fuelOC :: (Monad m) => Int -> OCAlgebra Int a m fuelOC initFuel = OCAlgebra isSat' refine' initFuel union' notStrongerThan'   where@@ -22,30 +26,34 @@     union'  c c'          = max c c'     notStrongerThan' c c' = return $ c >= c' +-- | @contramap f oca@ transforms an OCA of terms of type @a@ terms of type @b@,+--   by using @f@ to convert terms of @b@ to equivalent ones of @a@ contramap :: forall c a b m .      (b -> a)   -> OCAlgebra c a m   -> OCAlgebra c b m-contramap f aoc = aoc{refine = refine'}+contramap f oca = oca{refine = refine'}   where     refine' :: c -> b -> b -> c-    refine' c t1 t2 = refine aoc c (f t1) (f t2)+    refine' c t1 t2 = refine oca c (f t1) (f t2) +-- | @bimapConstraints to from oca@ yields an oca using @d@ to track constraints; @to@ and @from@ should+--   define an isomorphism between c and d bimapConstraints :: forall c d a m .      (c -> d)   -> (d -> c)   -> OCAlgebra c a m   -> OCAlgebra d a m-bimapConstraints to from aoc = OCAlgebra isSat' refine' (to (top aoc)) union' notStrongerThan'+bimapConstraints to from oca = OCAlgebra isSat' refine' (to (top oca)) union' notStrongerThan'   where     isSat' :: d -> m Bool-    isSat' c = isSat aoc (from c)+    isSat' c = isSat oca (from c)      refine' :: d -> a -> a -> d-    refine' c t1 t2 = to $ refine aoc (from c) t1 t2+    refine' c t1 t2 = to $ refine oca (from c) t1 t2      union' :: d -> d -> d-    union' c1 c2 = to $ union aoc (from c1) (from c2)+    union' c1 c2 = to $ union oca (from c1) (from c2)      notStrongerThan' :: d -> d -> m Bool-    notStrongerThan' c1 c2 = notStrongerThan aoc (from c1) (from c2)+    notStrongerThan' c1 c2 = notStrongerThan oca (from c1) (from c2)

@@ -15,9 +15,9 @@ import Language.REST.Types import Language.REST.SMT (ToSMTVar) -showHash :: Show a => a -> String-showHash = show . hash . show-+-- | @lift@ takes a representation of constraints on a WQO over @base@,+--   alongside a function used to generate constraints to permit a relation on terms @lifted@,+--   and returns the corresponding Ordering Constraints Algebra lift :: forall impl base lifted m . (ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted, Show base, Show (impl base)) =>      OC.WQOConstraints impl m   -> OC.ConstraintGen impl base lifted Identity

@@ -11,6 +11,7 @@ import GHC.Generics (Generic) import Language.REST.SMT +-- | The operators used in 'RuntimeTerm' and 'MetaTerm' newtype Op = Op Text deriving (Eq, Ord, Hashable, Generic)  instance Show Op where

@@ -8,25 +8,33 @@ import GHC.Generics (Generic) import Data.Hashable +-- | @Step@ represents an intermediate step in a 'Path' explored by REST data Step rule term a = Step {-    term     :: PathTerm rule term-  , rule     :: rule-  , ordering :: a-  , fromPLE  :: Bool+    term     :: PathTerm rule term -- ^ The "from" term in this path+  , rule     :: rule               -- ^ The rule generating the next term+  , ordering :: a                  -- ^ The generated constraints from applying the rule+  , fromPLE  :: Bool               -- ^ Whether the term was derived from a provably terminating eval function } deriving (Eq, Ord, Generic, Hashable)  +-- | @PathTerm@ is the term explored at a path data PathTerm rule term = PathTerm     {  pathTerm :: term+    ,  rejected :: S.HashSet (term, rule) -- ^ The orderings FROM pathTerm that were rejected.+                                          -- TODO: This should be removed, as it's really only used+                                          --       in the visualization -       -- The orderings FROM pathTerm that were rejected-    ,  rejected :: S.HashSet (term, rule)     } deriving (Eq, Ord, Generic, Hashable) +-- | A path explored by REST.+-- The head of the 1st part of the tuple is the initial term.+-- The 2nd part of the tuple is the last term. type Path rule term a = ([Step rule term a], PathTerm rule term) +-- | Extracts the list of terms from the path pathTerms :: Path rule term a -> [term] pathTerms (xs, x) = map pathTerm $ map term xs ++ [x] +-- | Extracts the last (most recently generated) term runtimeTerm :: Path rule term a -> term runtimeTerm (_, pt) = pathTerm pt

@@ -1,8 +1,15 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-module Language.REST.RESTDot where +-- | This module is responsible for rendering GraphViz graphs corresponding to an+--   execution of the REST algorithm.+module Language.REST.RESTDot (+    PrettyPrinter(..)+  , ShowRejectsOpt(..)+  , writeDot+  ) where+ import Data.List import Data.Hashable import qualified Data.Set as S@@ -11,10 +18,14 @@ import Language.REST.Dot import Language.REST.Path +-- | Controls how rejected paths should be visualized data ShowRejectsOpt =-  ShowRejectsWithRule | ShowRejectsWithoutRule | HideRejects+    ShowRejectsWithRule     -- ^ Display rejected paths, and the rule that generated them+  | ShowRejectsWithoutRule  -- ^ Display rejected paths, but don't display the rule that generated them+  | HideRejects             -- ^ Do not show rejected paths   deriving Eq +-- | Controls how rules, terms, orderings, and rejected paths should be displayed data PrettyPrinter rule term ord = PrettyPrinter   { printRule    :: rule -> String   , printTerm    :: term -> String@@ -102,6 +113,7 @@       unions :: (Ord a, Eq a, Hashable a) => S.Set (S.Set a) -> S.Set a       unions = S.unions . S.toList +-- | @writeDot name gt printer paths@ generates a graphViz graph from @paths@ with name @name@. writeDot :: (Hashable rule, Hashable term, Ord a, Hashable a) =>   String -> GraphType -> PrettyPrinter rule term a -> S.Set (Path rule term a) -> IO () writeDot name gt printer paths = mkGraph name (toGraph gt printer paths)

@@ -6,7 +6,9 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ImplicitParams #-} -module Language.REST.RPO (rpo, rpoTerm, rpoGTE, rpoGTE', synGTE) where+-- | This module contains the implementation of the Recursive Path Quasi-Ordering,+--   defined in section 4.2.1 of the REST paper+module Language.REST.RPO (rpo, rpoGTE, synGTE) where  import Prelude hiding (EQ, GT) @@ -75,6 +77,8 @@       modify (\st -> st{ rpoCache = M.insert key result (rpoCache st)})       return result +-- | The constraint generator for RPQO. That is, given terms @t@, @u@, @rpo@ generates+--   the constraints on n RPQO ≥ᵣ such that t ≥ᵣ u. rpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RT.RuntimeTerm Identity rpo = runStateConstraints (cmapConstraints rpoTerm rpo') (RPOState M.empty 0) @@ -102,6 +106,8 @@         , rpoMul oc GTE cs'                             ts               (MS.singleton u)         ] +-- | @rpoGTE impl t u@ generates the constraints a WQO over 'Op' (via @impl@) that ensures+--   that t ≥ᵣ u in the result RPQO ≥ᵣ. rpoGTE   :: (?impl::WQOConstraints oc m, Hashable (oc Op), Eq (oc Op), Show (oc Op))   => RT.RuntimeTerm@@ -124,6 +130,8 @@ synEQ :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool synEQ o l r = synGTE' o l r && synGTE' o r l +-- | Performs the (concrete) RPQO calculation. @synGTE o t u@ returns+--   true iff t ≥ᵣ u using an RPQO with precedence @o@. synGTE :: OpOrdering -> RT.RuntimeTerm -> RT.RuntimeTerm -> Bool synGTE o t u = synGTE' o (rpoTerm t) (rpoTerm u) 

@@ -6,18 +6,20 @@ {-# LANGUAGE NamedFieldPuns #-} {-# OPTIONS_GHC -Wno-error=deprecations #-} +-- | This module contains the core REST algorithm module Language.REST.Rest (     rest   , pathsResult   , termsResult-  , terms   , PathsResult(..)+  , TermsResult   , WorkStrategy(..)   , RESTParams(..)+  , RESTResult(..)   ) where  import           Control.Monad-import           Control.Monad.List+import           Control.Monad.Trans import Data.Hashable import qualified Data.HashSet as S import qualified Data.List    as L@@ -28,30 +30,40 @@ 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 = PathsResult S.empty +-- | An initial (empty) instance of 'TermsResult' termsResult :: TermsResult rule term oc termsResult = TermsResult 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-  terms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term+  -- | Obtains the terms explored by REST+  resultTerms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term  instance RESTResult PathsResult where   includeInResult p (PathsResult s) = PathsResult (S.insert p s)-  terms (PathsResult s) = S.fromList (concatMap pathTerms $ S.toList s)-+  resultTerms (PathsResult s) = S.fromList (concatMap pathTerms $ S.toList s)  instance RESTResult TermsResult where   includeInResult p (TermsResult s) = TermsResult (S.union s (S.fromList $ pathTerms p))-  terms (TermsResult s)             = s+  resultTerms (TermsResult s)       = s   data RESTState m rule term oc et rtype = RESTState@@ -71,6 +83,7 @@   , 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

@@ -4,5 +4,10 @@  import qualified Data.HashSet as S +-- | A class for datatypes that can be used as rewrite rules class RewriteRule m rule term where+  -- | @apply term rule@ returns the set of resulting terms that can be generated+  --   from @term@ using @rule@. Multiple terms are possible if the rule applies to+  --   multiple subterms. The result is embedded in a computation context @m@;+  --   this enables support for SMT-based conditional rewriting, for example.   apply :: term -> rule -> m (S.HashSet term)

@@ -1,7 +1,13 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} -module Language.REST.RuntimeTerm where+module Language.REST.RuntimeTerm+  ( RuntimeTerm(..)+  , ToRuntimeTerm(..)+  , subTerms+  , contains+  )+where  import           Data.Hashable import           GHC.Generics (Generic)@@ -10,12 +16,14 @@  import           Language.REST.Op +-- | Ground terms data RuntimeTerm = App Op [RuntimeTerm] deriving (Eq, Ord, Generic, Hashable)  instance Show RuntimeTerm where   show (App op []) = show op   show (App op ts) = printf "%s(%s)" (show op) $ L.intercalate ", " (map show ts) +-- | Transformable to a ground term class ToRuntimeTerm a where   toRuntimeTerm :: a -> RuntimeTerm @@ -25,6 +33,11 @@ instance ToRuntimeTerm RuntimeTerm where   toRuntimeTerm = id +-- | @subTerms t@ returns a list of pairs @(s, f)@, where @s@ is a subterm of @t@,+-- and @f@ is a function that takes a replacement @s'@ for @s@, and generates a new+-- term where @s@ is replaced with @s'@ in @t@. Also includes the pair (t, id),+-- representing the term itself.+-- TODO: Consider more efficient implementations subTerms :: RuntimeTerm -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))] subTerms t@(App f ts) = (t, id) : concatMap st [0..length ts - 1]   where@@ -37,3 +50,9 @@         go2 (srt, toFull) = (srt, go . toFull)       in         map go2 (subTerms ti)+++-- | @t `contains` u@ iff @t == u@ or @u@ is a subterm of @t@+contains :: RuntimeTerm -> RuntimeTerm -> Bool+contains t1 t2 | t1 == t2 = True+contains (App _ ts) t     = any (contains t) ts

@@ -12,7 +12,29 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} -module Language.REST.SMT where+-- | This module contains functionality for creating SMTLIB expressions and interacting+--   with an SMT solver.+module Language.REST.SMT+  (+    checkSat+  , checkSat'+  , getModel+  , parseModel+  , killZ3+  , spawnZ3+  , smtAdd+  , smtAnd+  , smtFalse+  , smtGTE+  , smtTrue+  , withZ3+  , SolverHandle+  , SMTExpr(..)+  , SMTVar(..)+  , ToSMT(..)+  , ToSMTVar(..)+  , Z3Model+) where  import Control.Monad.IO.Class import Data.Hashable@@ -27,6 +49,8 @@ import GHC.Generics (Generic) import GHC.IO.Handle +-- | A model returned by Z3 corresponding to a satisfiable+--   set of constraints. Untyped. type Z3Model = M.Map String String  parens :: Text.Parsec.Prim.Stream s m Char => ParsecT s u m a -> ParsecT s u m a@@ -54,23 +78,16 @@   defs <- endBy parseFunDef spaces   return $ M.fromList defs -readModel :: Handle -> IO String-readModel handle = go "" where-  closedTerm t = length (filter (== '(') t) == length (filter (== ')') t)-  go buf = do-    line <- hGetLine handle-    let buf' = buf ++ line ++ "\n"-    if closedTerm buf'-    then return buf'-    else go buf'-+-- | Parses Z3's model string into a 'Z3Model'. parseModel :: String -> Z3Model parseModel str = case parse modelParser "" str of   Left err -> error (show err)   Right t  -> t +-- | An SMT variable newtype SMTVar a = SMTVar T.Text deriving (Eq, Ord) +-- | SMTLib expressions data SMTExpr a where     And     :: [SMTExpr Bool] -> SMTExpr Bool     Add     :: [SMTExpr Int]  -> SMTExpr Int@@ -153,16 +170,20 @@ smtTrue :: SMTExpr Bool smtTrue  = And [] +-- | Returns an SMT expression that adds all elements in the list. If the list is empty,+--   returns @Const 0@. smtAdd :: [SMTExpr Int] -> SMTExpr Int smtAdd [] = Const 0 smtAdd ts = Add ts +-- | `smtAnd t u` returns an smt expression representing \( t \land u \). smtAnd :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool smtAnd (And xs) (And ys) = And $ L.nub (xs ++ ys) smtAnd (And xs) e        = And $ L.nub (xs ++ [e]) smtAnd e        (And ys) = And $ L.nub (e:ys) smtAnd t        u        = And [t, u] +-- | `smtGTE t u` returns an SMT expression \( t \geqslant u \). If @t == u@, returns 'smtTrue'. smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool smtGTE t u | t == u    = smtTrue smtGTE t u | otherwise = GTE t u@@ -195,17 +216,22 @@ askCmds expr = varDecls ++ [SMTAssert expr, CheckSat] where   varDecls = map DeclareVar $ S.toList (vars expr) +-- | The handle (stdIn, stdOut) used for interacting with Z3 type SolverHandle = (Handle, Handle) -spawnZ3 :: IO (Handle, Handle)+-- | Instantiates a Z3 instance, returning the solver handle for interaction+spawnZ3 :: IO SolverHandle spawnZ3 = do   (Just stdIn, Just stdOut, _, _) <- createProcess (proc "z3" ["-in"]) {std_in = CreatePipe, std_out = CreatePipe}   return (stdIn, stdOut) -killZ3 :: (Handle, b) -> IO ()+-- | Kills the Z3 instance by closing the standard input stream+killZ3 :: SolverHandle -> IO () killZ3 (stdIn, _) = hClose stdIn -withZ3 :: MonadIO m => ((Handle, Handle) -> m b) -> m b+-- | @withZ3 f@ instantiates a Z3 instance, runs @f@ with that instance,+--   and then closes the instance and returns the result+withZ3 :: MonadIO m => (SolverHandle -> m b) -> m b withZ3 f =   do     z3     <- liftIO $ spawnZ3@@ -213,11 +239,14 @@     liftIO $ killZ3 z3     return result +-- | @getModel@ instructs an instantiated SMT solver to produce its model. getModel :: Handle -> IO () getModel stdIn = do   hPutStr stdIn "(get-model)\n"   hFlush stdIn +-- | @checkSat' handles expr@ checks satisfiability of @expr@ in an instantiated SMT solver.+--   This is wrapped in a @push@ / @pop@, so it does not change the SMT environment checkSat' :: (Handle,  Handle) -> SMTExpr Bool -> IO Bool checkSat' (stdIn, stdOut) expr = do   sendCommands $ Push:askCmds expr@@ -237,6 +266,8 @@       hPutStr stdIn $ (T.unpack (T.intercalate "\n" (map commandString cmds))) ++ "\n"       hFlush stdIn +-- | @checkSat expr@ launches Z3, to checks satisfiability of @expr@, terminating Z3+--   afterwards. Just a utility wrapper for `checkSat'` checkSat :: SMTExpr Bool -> IO Bool checkSat expr = do   z3     <- spawnZ3@@ -244,9 +275,14 @@   killZ3 z3   return result +-- | This class allows elements of type @a@ to be used as SMT /vaiables/ of type @b@.+--   For example, the instance @ToSMTVar Op Int@ allows 'RuntimeTerm' operators to be+--   represented as 'Int' variables. class ToSMTVar a b | a -> b where   toSMTVar :: a -> SMTVar b +-- | This class allows elements of type @a@ to be used as SMT expressions of type+--   @b@ class ToSMT a b where   toSMT :: a -> SMTExpr b 

@@ -28,9 +28,20 @@ import           Language.REST.Op import           Language.REST.MetaTerm as MT +-- | Arguments used for pretty-printing terms data PPArgs = PPArgs-  { ppReplace  :: [(T.Text, T.Text)]+  {+    -- | A list of pairs @(search, rep)@. If any operator starts with @search@+    --   for some element in the list, during the printing the operator is+    --   printed with the corresponding @rep@ in place of @search@.+    ppReplace  :: [(T.Text, T.Text)]++    -- | A list of pairs @(search, rep)@. If any operator matches @search@, then it's+    --   corresponding term is printed in infix style with operator @rep@.   , ppInfixOps :: [(T.Text, T.Text)]++    -- | Used to override printing for some terms. When @ppCustom m = Just s@, then @m@+    --   be printed as @s@.   , ppCustom   :: MetaTerm -> Maybe T.Text   } 

@@ -1,13 +1,14 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE FlexibleContexts #-}++-- | This module includes a typeclass for implementations of constraints on 'WQO's module Language.REST.WQOConstraints   (     WQOConstraints(..)   , ConstraintGen   , liftC   , cmapConstraints-  , numOrderings   , isUnsatisfiable   , intersectAll   , unionAll@@ -20,7 +21,6 @@ import Control.Monad.State.Strict import qualified Data.List as L import Data.Hashable-import qualified Data.Set as S  import Prelude hiding (GT, EQ) @@ -30,45 +30,63 @@  type WQO = WQO.WQO -trace' :: String -> a -> a-trace' _ x = x-+-- | @WQOConstraints impl m@ defines an implementation for tracking and checking+--   satisfiability of constraints on arbitrary type @a@. Namely, instances of+--   @impl a@ are used to keep track of constraints. Satisfiability checking and+--   other computations are embedded in a computational context @m@. data WQOConstraints impl m = OC-  { addConstraint       :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a+  {+    -- | @addConstraint wqo c@ adds constraints to @c@ to also permit the WQO @w@.+    addConstraint       :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a++    -- | @intersect c1 c2@ returns constraints to permit only WQOs permitted by both @c1@ and+    --   @c2@. Therefore the resulting constraints are stronger (less likely to be+    --   satisifiable).   , intersect           :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a+    -- | @isSatisfiable c@ returns true iff @c@ permits any WQO   , isSatisfiable       :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool++    -- | @c1 `notStrongerThan` c2@ iff any ordering permitted by @c1@ is also permitted+    --   by @c2@   , notStrongerThan     :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool+    -- | @noConstraints@ returns an instance of constraints that permits any WQO   , noConstraints       :: forall a. (Eq a, Ord a, Hashable a) => impl a+   , permits             :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> WQO a -> Bool-  , relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a -> S.Set a -> impl a+    -- | @c1 `union` c2@ returns constraints that permit WQOs permitted by /either/+    --  @c1@ or @c2@. The resulting constraints are therefore weaker (more likely to+    --  be satisfiable)   , union               :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a++    -- | @unsatisfiable@ returns an instance of constraints that does not permit any WQO   , unsatisfiable       :: forall a. impl a-  , elems               :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a++    -- | @getOrdering c@ returns a concrete ordering satisfying the constraints, if one exists   , getOrdering         :: forall a. impl a -> Maybe (WQO a)-  , simplify            :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a   } -numOrderings :: (Show a, Ord a, Eq a, Ord a, Hashable a) => S.Set a -> WQOConstraints oc m -> oc a -> Int-numOrderings elems impl oc = S.size $ S.filter (permits impl oc) (WQO.orderings elems)-+-- | Returns true iff the constraints do not permit any WQO. isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool isUnsatisfiable OC{isSatisfiable} c = not <$> isSatisfiable c +-- | Returns the constraints that permit a given WQO singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a singleton OC{addConstraint, noConstraints} c = addConstraint c noConstraints +-- | Given a list of constraints @ocs@, returns constraints that permit only the WQOs+--   permitted by each @oc@ in @ocs@ intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a intersectAll OC{noConstraints} []     = noConstraints-intersectAll OC{intersect}     (x:xs) = L.foldl' go x xs-  where-    go t1 t2 = trace' ("Intersect " ++ (show t1)) $ intersect t1 t2+intersectAll OC{intersect}     (x:xs) = L.foldl' intersect x xs +-- | Given a list of constraints @ocs@, returns constraints that permit the WQOs+--   permitted by any @oc@ in @ocs@ unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a unionAll OC{unsatisfiable} []     = unsatisfiable-unionAll OC{union}         (x:xs) = L.foldl' go x xs-  where-    go t1 t2 = trace' ("Union " ++ (show t1)) $ union t1 t2+unionAll OC{union}         (x:xs) = L.foldl' union x xs +-- | @intersectRelation oc impl (f, g, r)@ strengthens constraints represented by @impl@+--   to also ensure that @f@ and @g@ are related via relation @r@ in permitted WQOs. intersectRelation ::   (Ord a, Eq a, Ord a, Hashable a, Show a) =>   WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a@@ -84,21 +102,21 @@       wqo2 <- WQO.singleton (f, g, WQO.QEQ)       return $ union oc (singleton oc wqo1) (singleton oc wqo2) ----- ConstraintGen impl R >= t u returns the constraints on >= that guarantee+-- | ConstraintGen impl R >= t u returns the constraints on >= that guarantee -- the resulting relation >=', we have: --   1. x >= y implies x >=' y --   2. t lift(R(>=')) u -- Where R generates { == , >=, > } from the underlying ordering -- R is used to enable optimizations- type ConstraintGen oc base lifted m =   forall m' . (WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base)) +-- | @cmapConstraints@ takes a transformation @f@ from @lifted' to lifted@, and transforms+-- a constraint generator on terms of types @lifted@ into one on terms of types @lifted'@ cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m cmapConstraints f cgen impl r oc t u = cgen impl r oc (f t) (f u) +-- | @liftc f imp@ lifts the computations of @imp@ from context @m@ to context @m'@ liftC :: (m Bool  -> m' Bool) -> WQOConstraints impl m -> WQOConstraints impl m' liftC f oc = oc{     isSatisfiable   = isSatisfiable'@@ -108,5 +126,7 @@     isSatisfiable'   c1    = f (isSatisfiable oc c1)     notStrongerThan' c1 c2 = f (notStrongerThan oc c1 c2) +-- @runStateConstriants initState cgen@ transforms a constraint generator in the 'State'+-- monad to one in the 'Identity' monad by using initial state @initState@' runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity runStateConstraints cgen initState impl r oc t u = Identity $ evalState (cgen impl r oc t u) initState

@@ -7,11 +7,17 @@  #define OPTIMIZE_WQO -module Language.REST.WQOConstraints.ADT where+module Language.REST.WQOConstraints.ADT+  (  ConstraintsADT(..)+  , addConstraint+  , adtOC+  , intersect+  , union+  )+where  import GHC.Generics (Generic) -import Debug.Trace import Data.Hashable import Control.Monad.State.Lazy import qualified Data.Set as S@@ -26,10 +32,14 @@  type WQO = WQO.WQO +-- | Represents constraints over a WQO on @a@ data ConstraintsADT a =+ -- | @Sat wqo@ represents satisfiable constraints: those that permit each relation in @wqo@.     Sat (WQO a)   | Unsat+    -- | @Union c1 c2@ permits orderings of P1 and orderings of P2   | Union (ConstraintsADT a) (ConstraintsADT a)+    -- | @Intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2   | Intersect (ConstraintsADT a) (ConstraintsADT a)   deriving (Eq, Ord, Generic, Hashable) @@ -46,16 +56,7 @@ cost (Sat wqo)           = S.size $ WQO.elems wqo cost Unsat               = 100 -minDepth :: ConstraintsADT a -> Int-minDepth (Union lhs rhs)     = 1 + min (minDepth lhs) (minDepth rhs)-minDepth (Intersect lhs rhs) = 1 + min (minDepth lhs) (minDepth rhs)-minDepth _                   = 1--maxDepth :: ConstraintsADT a -> Int-maxDepth (Union lhs rhs)     = 1 + max (maxDepth lhs) (maxDepth rhs)-maxDepth (Intersect lhs rhs) = 1 + max (maxDepth lhs) (maxDepth rhs)-maxDepth _                   = 1-+-- | @intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2 intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a  #ifdef OPTIMIZE_WQO@@ -92,6 +93,7 @@ #endif intersect t1 t2            = Intersect t1 t2 +-- | @union c1 c2@ permits orderings of P1 and orderings of P2 union :: Eq a => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a union (Sat w) _            | w == WQO.empty = Sat w union _            (Sat w) | w == WQO.empty = Sat w@@ -103,14 +105,11 @@ union c1 c2 | c1 == c2 = c1 union c1 c2            = Union c1 c2 +-- | @addConstraint o c@ strengthes @c@ to also contain every relation in @o@ addConstraint  :: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a addConstraint o c = intersect (Sat o) c -relevantConstraints-  :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> S.Set a -> S.Set a -> ConstraintsADT a-relevantConstraints c _ _ = c- notStrongerThan   :: (Eq a, ToSMTVar a Int)   => ConstraintsADT a@@ -126,9 +125,6 @@ unsatisfiable :: ConstraintsADT a unsatisfiable = Unsat -trace' :: String -> a -> a-trace' = trace- {-# SPECIALIZE getConstraints :: ConstraintsADT Op -> [WQO Op] #-} getConstraints :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> [WQO a] getConstraints adt = -- trace' ("Get constraints, size : " ++ (show $ dnfSize adt)) $@@ -199,28 +195,6 @@         then (lhs, rhs)         else (rhs, lhs) -dnfSize :: ConstraintsADT a -> Int-dnfSize (Sat _w)       = 1-dnfSize Unsat         = 0-dnfSize (Union w1 w2) = dnfSize w1 + dnfSize w2-dnfSize (Intersect w1 w2) = dnfSize w1 * dnfSize w2---- toDNF (Union lhs rhs) = S.union (toDNF lhs) (toDNF rhs)--- toDNF (Intersect lhs rhs) =---   let---     ldnf = toDNF lhs---     rdnf = toDNF rhs---   in---     S.unions--simplify :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a-simplify _adt = undefined--- simplify adt = case getConstraints adt of---   []     -> Unsat---   (x:xs) -> foldl go (Sat x) xs---   where---     go a x = Union (Sat x) a- permits   :: (Ord a, Hashable a, Show a)   => ConstraintsADT a@@ -230,23 +204,14 @@  isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool isSatisfiable s = toSMT s-  -- trace (show (minDepth s) ++ " " ++ show (maxDepth s)) $ not $ null $ getConstraints s  instance (Eq a, Hashable a,  Show a) => Show (ConstraintsADT a) where-  -- show s = go 0 s where-  --   go n (Sat w)         = indent n $ show w-  --   go n Unsat           = indent n $ "⊥"-  --   go n (Union w t )    = indent n $ printf "∪\n%s\n%s" (go (n+1) w) (go (n+1) t)-  --   go n (Intersect w t) = indent n $ printf "∩\n%s\n%s" (go (n+1) w) (go (n+1) t)--  --   indent 0 s = s-  --   indent n s = take (n - 1) (repeat '|') ++ '+':s-   show (Sat w)         = show w   show Unsat           = "⊥"   show (Union w t )    = printf "(%s ∨\n %s)" (show w) (show t)   show (Intersect w t) = printf "(%s ∧ %s)" (show w) (show t) +-- | See 'ConstraintsADT' adtOC :: (Handle, Handle) -> OC.WQOConstraints ConstraintsADT IO adtOC z3 = OC.liftC (checkSat' z3) adtOC' @@ -258,9 +223,6 @@   notStrongerThan   noConstraints   permits-  relevantConstraints   union   unsatisfiable   undefined-  undefined-  simplify

@@ -3,22 +3,20 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} +-- | This module defines "Lazy" constraints on a WQO; the intention is that+--   computations on this type do only the necessary amount of work to determine+--   satisfiability (deferring further computations in a thunk). module Language.REST.WQOConstraints.Lazy (       lazyOC     , addConstraint-    , intersect     , isSatisfiable     , noConstraints-    , singleton-    , union-    , unsatisfiable     , LazyOC     ) where  import Text.Printf import GHC.Generics (Generic) import Data.Hashable-import qualified Data.Set as S  import qualified Language.REST.Internal.WQO as WQO import qualified Language.REST.WQOConstraints as OC@@ -31,8 +29,11 @@  type Thunk a = ADT.ConstraintsADT a +-- | Implementation of "Lazy" ordering constraints. data LazyOC a =     Unsat+    -- @Sat wqo thunk@ represent satisfiable constraints; @wqo@ is a candidate.+    -- @Thunk@ represents the other satisfiable constraints, if any.   | Sat (WQO a) (Thunk a)   deriving (Eq, Ord, Generic, Hashable) @@ -44,14 +45,9 @@ eval (ADT.Sat w)   = Sat w ADT.Unsat eval ADT.Unsat     = Unsat eval (ADT.Union lhs rhs) =-  case eval t1 of-    Sat w t1' -> Sat w (ADT.union t1' t2)-    Unsat     -> eval t2-  where-    (t1, t2) = (lhs, rhs)-      -- if ADT.minDepth lhs < ADT.minDepth rhs-      -- then (lhs, rhs)-      -- else (rhs, lhs)+  case eval lhs of+    Sat w t1' -> Sat w (ADT.union t1' rhs)+    Unsat     -> eval rhs  eval (ADT.Intersect t1 t2)       =   case (eval t1, eval t2) of@@ -76,6 +72,7 @@   show Unsat     = "⊥"   show (Sat s r) = printf "%s ∨ lazy(%s)" (show s) (show r) +-- | Returns a new instance of 'LazyOC' permitting all WQOs noConstraints :: LazyOC a noConstraints = Sat (WQO.empty) ADT.Unsat @@ -92,28 +89,24 @@ intersect :: (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a intersect t1 t2 = eval $ ADT.intersect (toADT t1) (toADT t2) +-- | Returns @true@ if any orderings are permitted isSatisfiable :: LazyOC a -> Bool isSatisfiable (Sat _ _) = True isSatisfiable Unsat     = False -singleton :: WQO a -> LazyOC a-singleton c = Sat c ADT.Unsat--relevantConstraints-  :: (Eq a, Ord a, Hashable a) => LazyOC a -> S.Set a -> S.Set a -> LazyOC a-relevantConstraints c _ _ = c- notStrongerThan :: (Monad m, Eq a) => LazyOC a -> LazyOC a -> m Bool notStrongerThan _     Unsat = return True notStrongerThan t1    t2    = return $ t1 == t2 -addConstraint :: (Ord a, Hashable a) => ADT.WQO a -> LazyOC a -> LazyOC a+-- | @addConstraint o c@ strengthes @c@ to also contain every relation in @o@+addConstraint :: (Ord a, Hashable a) => WQO a -> LazyOC a -> LazyOC a addConstraint o c = eval $ ADT.addConstraint o (toADT c)  permits :: (Ord a, Hashable a) => LazyOC a -> WQO.WQO a -> Bool permits Unsat _            = False permits (Sat s1 thunk) wqo = s1 `WQO.notStrongerThan` wqo || permits (eval thunk) wqo +-- | See 'LazyOC' lazyOC :: Monad m => OC.WQOConstraints LazyOC m lazyOC = OC.OC   addConstraint@@ -122,9 +115,6 @@   notStrongerThan   noConstraints   permits-  relevantConstraints   union   unsatisfiable-  undefined   getOrdering-  id

@@ -3,24 +3,17 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} +-- | This module defines an implemenation for representing constraints on a 'WQO';+--   in this case represented by a set of "extendable" WQOs each satisfying the constraints.+--   For more details see 'StrictOC' module Language.REST.WQOConstraints.Strict (       strictOC     , strictOC'-    , addConstraint     , difference-    , getOrdering-    , intersect-    , isSatisfiable     , isUnsatisfiable     , noConstraints-    , notStrongerThan     , permits-    , relevantConstraints-    , union-    , unsatisfiable-    , singleton     , StrictOC-    , elems     ) where  import Control.Monad.Identity@@ -40,7 +33,19 @@ -- The constraints are represented as a set ws of WQOs -- The constraints permit any WQO w that is a valid extension of some (w' in wqos) -+-- | @StrictOC ws@ represents constraints on a WQO. Each element of @ws@ is a WQO+--   that satisfies the constraints. @StrictOC ws@ permits a WQO @w@ if there exists+--   a @w'@ in @ws@ such that @w'@ can be extended to yield @w@.+--+--   This implementation is similar to disjunctive normal form representation of+--   logical formulas; except in this case each "conjunction" is a valid WQO, and thus+--   "satisfiable". Therefore @StrictOC ws@ satisfies /some/ WQO iff @ws@ is not empty.+--+--   Two potential downsides to this implementation are:+--   1. The size of @ws@ can grow quickly; an inherent issue of DNF+--   2. Related, calculating the entire set @ws@ is computationally expensive,+--      and often unnecessary for RESTs use-case, where continuing the path only+--      requires knowing if /any/ WQO is permitted. data StrictOC a = StrictOC (S.Set (WQO a))   deriving (Eq, Ord, Generic, Hashable) @@ -48,22 +53,20 @@   show (StrictOC cs) | S.null cs             = "unsatisfiable"   show (StrictOC cs) | S.member WQO.empty cs = "no constraints"   show (StrictOC cs) = L.intercalate " ∨ \n" (map show (S.toList cs))-    -- where-      -- show' o@(OpOrdering s) = if S.size s > 1 then printf "(%s)" (show o) else show o  getOrdering :: StrictOC a -> Maybe (WQO a) getOrdering (StrictOC o) =   listToMaybe (S.toList o) -elems :: Ord a => StrictOC a -> S.Set a-elems (StrictOC sets) = S.unions $ map WQO.elems (S.toList sets)-+-- | Constraints that permit any 'WQO'. In this case implemented by+--   a singleton set containing an empty WQO. noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a noConstraints = StrictOC (S.singleton (WQO.empty))  unsatisfiable :: StrictOC a unsatisfiable = StrictOC S.empty +-- | Returns @true@ iff @strictOC ws@ does not permit any WQOs; i.e., if @ws@ is empty. isUnsatisfiable :: Eq a => StrictOC a -> Bool isUnsatisfiable c = c == unsatisfiable @@ -96,8 +99,8 @@             else go (x : include) xs  --- The intersection of two constraints `a` and `b` is new constraints that only--- permits the orderings permitted by both `a` and `b`+-- | The intersection of two constraints `a` and `b` is new constraints that only+--   permits the orderings permitted by both `a` and `b` intersect :: (Show a, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a intersect (StrictOC lhs) (StrictOC rhs) = result   -- trace (printf "%s intersect %s yields %s" (show lhs) (show rhs) (show result)) result@@ -113,26 +116,13 @@   c'  <-  S.toList oc   maybeToList $ WQO.merge c c' -singleton :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a-singleton c = addConstraint c noConstraints--relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> S.Set a -> S.Set a -> StrictOC a-relevantConstraints (StrictOC oc0) as bs = go (S.toList oc0) unsatisfiable-  where-    go :: [WQO a] -> StrictOC a -> StrictOC a-    go []          oc   = oc-    go (o : rest) exist =-      let-        o' = WQO.relevantTo o as bs-      in-        if WQO.null o'-        then noConstraints-        else go rest (union (singleton o) exist)-+-- | @StrictOC ws@ permits a 'WQO' @w@ if there exists a @w'@ in @ws@+--   that can be extended to equal @w@ permits :: (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool permits (StrictOC permitted) desired =   any (`WQO.notStrongerThan` desired) (S.toList permitted) +-- | An implementation of 'StrictOC'; for any computational context strictOC :: Monad m => OC.WQOConstraints StrictOC m strictOC = OC.OC   addConstraint@@ -141,12 +131,11 @@   notStrongerThan   noConstraints   permits-  relevantConstraints   union   unsatisfiable-  elems   getOrdering-  id +-- | An implementation of 'StrictOC' in the 'Identity' monad; usable in pure+--   computations. strictOC' :: OC.WQOConstraints StrictOC Identity strictOC' = strictOC

@@ -36,9 +36,11 @@ import Language.REST.Op import Language.REST.RPO import Language.REST.Internal.OpOrdering+import Language.REST.RewriteRule import Language.REST.RuntimeTerm import Language.REST.MetaTerm as MT import Language.REST.Internal.Rewrite+import Language.REST.Internal.WQO import Language.REST.Rest import Language.REST.SMT import qualified Language.REST.WQOConstraints.ADT as AC@@ -46,6 +48,13 @@ import qualified Data.Maybe as Mb import qualified Data.HashSet as S ++-- | 'canOrient' returns true iff the ordering constraint algebra permits an ordering+--   that orients, the path, i.e., the constraints generated by 'orient' are satisfiable.+canOrient :: forall oc m . Show oc+  => (?impl :: OCAlgebra oc RuntimeTerm m) => [RuntimeTerm] -> m Bool+canOrient terms = isSat ?impl (orient ?impl terms)+ diverges :: (Show oc) => OCAlgebra oc RuntimeTerm IO -> [RuntimeTerm] -> IO Bool diverges impl ts = not <$> (isSat impl $ orient impl ts) @@ -53,7 +62,7 @@   => OCAlgebra oc RuntimeTerm IO   -> S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm) rewrites impl evalRWs userRWs t0 =-  terms <$> fst <$> rest+  resultTerms <$> fst <$> rest     RESTParams       { re           = evalRWs       , ru           = userRWs@@ -115,6 +124,14 @@     return $ not $ disjoint rw1 rw2   where     disjoint s1 s2 = S.null $ s1 `S.intersection` s2++eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm+eval rws t0 =+  do+    result <- mapM (apply t0) (S.toList rws)+    case S.toList $ S.unions result of+      []      -> return t0+      (t : _) -> eval rws t  arithTests :: (Show oc, Hashable oc, Eq oc) => OCAlgebra oc RuntimeTerm IO -> [(String, IO Bool)] arithTests impl =