rest-rewrite 0.4.0 → 0.4.1

raw patch · 42 files changed

+223/−229 lines, 42 filesdep ~hashabledep ~mtldep ~text

Dependency ranges changed: hashable, mtl, text, time

Files

• rest-rewrite.cabal +8/−8
• src/Language/REST/Dot.hs +5/−5
• src/Language/REST/ExploredTerms.hs +5/−5
• src/Language/REST/Internal/ListT.hs +2/−3
• src/Language/REST/Internal/MultiSet.hs +4/−4
• src/Language/REST/Internal/MultisetOrder.hs +7/−7
• src/Language/REST/Internal/OpOrdering.hs +3/−3
• src/Language/REST/Internal/PartialOrder.hs +3/−3
• src/Language/REST/Internal/Rewrite.hs +3/−2
• src/Language/REST/Internal/WQO.hs +21/−22
• src/Language/REST/KBO.hs +2/−2
• src/Language/REST/LPO.hs +9/−9
• src/Language/REST/OCAlgebra.hs +1/−1
• src/Language/REST/OCToAbstract.hs +1/−2
• src/Language/REST/RESTDot.hs +3/−3
• src/Language/REST/RPO.hs +3/−4
• src/Language/REST/Rest.hs +6/−6
• src/Language/REST/RuntimeTerm.hs +2/−2
• src/Language/REST/SMT.hs +9/−9
• src/Language/REST/Types.hs +4/−4
• src/Language/REST/WQOConstraints/ADT.hs +16/−17
• src/Language/REST/WQOConstraints/Lazy.hs +4/−4
• src/Language/REST/WQOConstraints/Strict.hs +2/−2
• test/BagExample.hs +8/−8
• test/Group.hs +1/−1
• test/Lists.hs +2/−2
• test/Main.hs +9/−9
• test/Multiset.hs +3/−3
• test/MultisetOrder.hs +2/−2
• test/NonTerm.hs +1/−1
• test/OpOrdering.hs +7/−7
• test/QuickCheckTests.hs +3/−3
• test/RPO.hs +6/−6
• test/StrictOC.hs +7/−7
• test/Test.hs +27/−25
• test/WQO.hs +2/−1
• testlib/Arith.hs +4/−4
• testlib/Language/REST/ConcreteOC.hs +1/−1
• testlib/Language/REST/ProofGen.hs +6/−9
• testlib/MultisetOrdering.hs +9/−11
• testlib/Nat.hs +1/−1
• testlib/Set.hs +1/−1

@@ -1,6 +1,6 @@ name:               rest-rewrite build-type:         Simple-version:            0.4.0+version:            0.4.1 cabal-version:      2.0 category:           Rewriting maintainer:         Zack Grannan <zgrannan@cs.ubc.ca>@@ -53,12 +53,12 @@   hs-source-dirs: src   build-depends:  base                 >= 4.7 && < 5                 , containers           >= 0.6.2 && < 0.7-                , hashable             >= 1.3.0 && < 1.4+                , hashable             >= 1.3.0 && < 1.5                 , process              >= 1.6.9 && < 1.7                 , parsec               >= 3.1.14 && < 3.2-                , mtl                  >= 2.2.2 && < 2.3+                , mtl                  >= 2.2.2 && < 2.4                 , unordered-containers >= 0.2.13 && < 0.3-                , text                 >= 1.2.4 && < 1.3+                , text                 >= 1.2.4 && < 2.1  library testlib   default-language:  Haskell2010@@ -72,8 +72,8 @@                 , mtl                 , monad-loops >= 0.4.3 && < 0.5                 , unordered-containers >= 0.2.11-                , text >= 1.2.2-                , time >= 1.9.3 && < 1.10+                , text+                , time >= 1.9.3 && < 1.13   exposed-modules:       Arith       DSL@@ -123,8 +123,8 @@                 , mtl                 , unordered-containers >= 0.2.11                 , testlib-                , text >= 1.2.2-                , time >= 1.9.3 && < 1.10+                , text+                , time                 -- , liquidhaskell                 -- , liquid-base   other-modules:

@@ -37,7 +37,7 @@   deriving (Read)  -- | A GraphViz node-data Node = Node +data Node = Node     { nodeID     :: NodeID     , label      :: String     , nodeStyle  :: String@@ -60,9 +60,9 @@  edgeString :: Edge -> String edgeString (Edge efrom eto elabel color esubLabel style) =-    let +    let         sub = escape esubLabel-        escape xs = concatMap go xs+        escape = concatMap go             where                 go '\\' = "\\"                 go '\n' = "<br />"@@ -77,8 +77,8 @@         printf "\t%s -> %s [label = <%s<br/>%s>\ncolor=\"%s\"\nstyle=\"%s\"];" efrom eto labelPart sub color style  graphString :: DiGraph -> String-graphString (DiGraph name nodes edges) = -    printf "digraph %s {\n%s\n\n%s\n}" name (nodesString) (edgesString)+graphString (DiGraph name nodes edges) =+    printf "digraph %s {\n%s\n\n%s\n}" name nodesString edgesString     where         nodesString :: String         nodesString = intercalate "\n" (map nodeString (S.toList nodes))

@@ -50,7 +50,7 @@ -- | 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+  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@@ -64,9 +64,9 @@ 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   where-    go (oc1, s1) (oc2, s2) = (union oc1 oc2, S.union s1 s2)+    go (oc1, s1) (oc2, s2) = (oc1 `union` oc2, S.union s1 s2) -lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, (S.HashSet term))+lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, S.HashSet term) lookup t (ET etMap _ _) = M.lookup t etMap  -- | @isFullyExplored t c M = not explorable(t, c)@ where @explorable@ is@@ -97,14 +97,14 @@                           -- 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'+                          ts    = S.union trms' (S.fromList rest) `S.difference` seen'                         in                           go seen' (S.toList ts)                   where                     seen' = S.insert (h, oc') seen    -- There exists a reachable term that has never previously been seen; not fully explored-  go _ _        | otherwise = return False+  go _ _         = 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@

@@ -5,14 +5,13 @@ import           Control.Applicative import           Control.Monad.Trans -data ListT m a = ListT {+newtype 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+    map f <$> mxs  instance (Monad m) => Applicative (ListT m) where   pure x                    = ListT (return [x])

@@ -26,7 +26,7 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S -data MultiSet a = MultiSet (M.HashMap a Int) deriving (Eq, Generic, Hashable, Ord)+newtype MultiSet a = MultiSet (M.HashMap a Int) deriving (Eq, Generic, Hashable, Ord)  instance Show a => Show (MultiSet a) where   show ms = "{" ++ L.intercalate ", " (map show $ toList ms) ++ "}"@@ -42,7 +42,7 @@ 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-deleteMany k _ (MultiSet ms) | otherwise = MultiSet $ M.delete k ms+deleteMany k _ (MultiSet ms)  = MultiSet $ M.delete k ms  distinctElems :: MultiSet a -> [a] distinctElems (MultiSet ms) = M.keys ms@@ -69,12 +69,12 @@ toList :: MultiSet a -> [a] toList ms = concatMap go (toOccurList ms)   where-    go (k, num) = take num $ repeat k+    go (k, num) = replicate num k  insert :: (Eq a, Hashable a) => a -> MultiSet a -> MultiSet a insert k (MultiSet ms) | Just c <- M.lookup k ms                        = MultiSet $ M.insert k (c + 1) ms-insert k (MultiSet ms) | otherwise+insert k (MultiSet ms)                        = MultiSet $ M.insert k 1 ms  singleton :: (Eq a, Hashable a) => a -> MultiSet a

@@ -25,10 +25,10 @@ trace' _ x = x  removeEQs :: (Eq x, Ord x, Hashable x) => MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x)-removeEQs ts0 us0 = go (M.toList ts0) M.empty us0 where+removeEQs ts0 = go (M.toList ts0) M.empty where   go []       ts us                   = (ts, us)   go (x : xs) ts us | x `M.member` us = go xs ts (M.delete x us)-  go (x : xs) ts us | otherwise       = go xs (M.insert x ts) us+  go (x : xs) ts us        = go xs (M.insert x ts) us  data Replace a =     ReplaceOne a a@@ -40,8 +40,8 @@ powerset (x:xs) = [x:ps | ps <- powerset xs] ++ powerset xs  possibilities :: (Hashable a, Eq a) => Relation -> [a] -> [a] -> S.HashSet (S.HashSet (Replace a))-possibilities r []     []    = if r == GT then S.empty else S.singleton (S.empty)-possibilities r xs     []    = if r == EQ then S.empty else S.singleton (S.fromList $ map (flip Replace S.empty)  xs)+possibilities r []     []    = if r == GT then S.empty else S.singleton S.empty+possibilities r xs     []    = if r == EQ then S.empty else S.singleton (S.fromList $ map (`Replace` S.empty)  xs) possibilities _ []     (_:_) = S.empty possibilities r (x:xs) ys    = if r == EQ then eqs else S.union eqs doms where   eqs = S.unions $ map go ys where@@ -60,7 +60,7 @@      ConstraintGen oc base lifted m   -> ConstraintGen oc base (MultiSet lifted) m multisetOrder _          impl _ oc _   _   | oc == unsatisfiable impl = return $ unsatisfiable impl-multisetOrder underlying impl r oc ts0 us0 = (uncurry go) (removeEQs ts0 us0) where+multisetOrder underlying impl r oc ts0 us0 = uncurry go (removeEQs ts0 us0) where   go :: MultiSet lifted -> MultiSet lifted -> m (oc base)   go ts us | M.null ts && M.null us             = return $ if r == GT then unsatisfiable impl else oc   go ts us | not (M.null ts) && M.null us       = return $ if r == EQ then unsatisfiable impl else oc@@ -71,7 +71,7 @@       pos = possibilities r (M.toList ts) (M.toList us)        result =-        trace' ("There are " ++ (show $ S.size pos) ++ " possibilities") $+        trace' ("There are " ++ show (S.size pos) ++ " possibilities") $         unionAll impl <$> mapM posConstraints (S.toList pos)        posConstraints pos1 = L.foldl' apply (return oc) (S.toList pos1) where@@ -82,4 +82,4 @@           oc' <- moc           if S.null ts'             then return oc'-            else intersectAll impl <$> (mapM (underlying impl GT oc' t) (S.toList ts'))+            else intersectAll impl <$> mapM (underlying impl GT oc' t) (S.toList ts')

@@ -1,7 +1,7 @@-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE DeriveAnyClass #-}++ {-# 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").

@@ -82,7 +82,7 @@     result = PartialOrder $ M.insertWith S.union f decs $ M.mapWithKey go m      go k old | S.member k ascs = S.union old decs-    go _ v   | otherwise       = v+    go _ v          = v      ascs = ascendants f o     decs = S.insert g $ descendents g o@@ -125,7 +125,7 @@    descs = S.unions (map (`descendents` po) froms) -  filtered = M.filterWithKey (\k _ -> not $ k `elem` froms) m+  filtered = M.filterWithKey (\k _ -> k `notElem` froms) m   m' =     if S.null descs     then filtered@@ -134,6 +134,6 @@   result = PartialOrder $ M.map go m'    go s | hasFrom s = S.insert to $ S.union descs $ S.difference s from'-  go s | otherwise = s+  go s  = s    hasFrom set = any (`S.member` set) froms

@@ -13,6 +13,7 @@  import GHC.Generics (Generic) +import           Data.Maybe (isNothing) import           Data.Hashable import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S@@ -61,7 +62,7 @@ unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst unify (MT.Var s) term su | M.lookup s su == Just term   = Just su-unify (MT.Var s) term su | M.lookup s su == Nothing+unify (MT.Var s) term su | isNothing (M.lookup s su)   = Just $ M.insert s term su unify (MT.RWApp o1 xs) (App o2 ys) su | o1 == o2 && length xs == length ys =   unifyAll su (zip xs ys)@@ -71,4 +72,4 @@   apply t (Rewrite left right _) = return $ S.unions $ map go (subTerms t)     where       go (t', tf) | Just su <- unify left t' M.empty = S.singleton (tf $ subst su right)-      go _        | otherwise                        = S.empty+      go _                                = S.empty

@@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}  module Language.REST.Internal.WQO (       empty@@ -86,10 +87,8 @@     show (WQO ecs po) = L.intercalate " ∧ " (map show ecs' ++ po')         where             ecs'          = filter (not . EC.isSingleton) $ S.toList ecs-            po'           = -                if PO.isEmpty po -                    then []-                    else [show po]+            po'           =+                [show po | not (PO.isEmpty po)]             --         else [show $ PO.mapUnsafe ecHead po]             -- ecHead (x, y) = (EC.head x, EC.head y) @@ -100,7 +99,7 @@ empty = WQO S.empty PO.empty  singleton :: (Ord a, Eq a, Hashable a) => (a, a, QORelation) -> Maybe (WQO a)-singleton t = insertMaybe empty t+singleton = insertMaybe empty  {-# INLINE elems #-} elems :: (Ord a) => WQO a -> S.Set a@@ -133,7 +132,7 @@     t <- L.find (EC.isMember source) classes'     if EC.isMember target t       then return (t, t)-      else ((,) t) <$> L.find (EC.isMember target) classes'+      else (t,) <$> L.find (EC.isMember target) classes'   where     classes' = S.toList classes @@ -142,12 +141,12 @@ {-# INLINE getRelation #-} getRelation :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a -> Maybe QORelation getRelation _ f g | f == g = Just QEQ-getRelation wqo@(WQO _ po) source target +getRelation wqo@(WQO _ po) source target     | Just (s, t) <- getEquivalenceClasses' wqo source target     = if s == t         then Just QEQ-        else -            if PO.gt po s t +        else+            if PO.gt po s t                 then Just QGT                 else Nothing     | otherwise = Nothing@@ -192,7 +191,7 @@     let       Just ec' = M.lookup ec ecsMap     in-      descs `S.isSubsetOf` (PO.descendents ec' po')+      descs `S.isSubsetOf` PO.descendents ec' po'   @@ -211,16 +210,16 @@ merge :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a) merge lhs@(WQO ecs po) rhs@(WQO ecs' po') | S.disjoint (elems lhs) (elems rhs)   = Just $ WQO (S.union ecs ecs') (PO.unionDisjointUnsafe po po')-merge lhs rhs | otherwise =+merge lhs rhs  =   if S.size (elems lhs) >= S.size (elems rhs)   then merge' lhs rhs   else merge' rhs lhs  {-# SPECIALISE merge' :: WQO Op -> WQO Op -> Maybe (WQO Op) #-} merge' :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a)-merge' lhs rhs@(WQO ecs po) = trace' message $ result where+merge' lhs rhs@(WQO ecs po) = trace' message result where -    message = "Merge " ++ (show $ hash lhs) ++ " " ++ (show $ hash rhs)+    message = "Merge " ++ show (hash lhs) ++ " " ++ show (hash rhs)      withEQs' = go lhs ecsFacts @@ -235,10 +234,10 @@         let             xs = EC.toList ec         in-            map (\(a, b) -> (a, b, QEQ)) (zip xs (tail xs))+            zipWith (\ a b -> (a, b, QEQ)) xs (tail xs)      poFacts :: [(a, a, QORelation)]-    poFacts = +    poFacts =         map (\(a, b) -> (head (EC.toList a), head (EC.toList b), QGT)) (PO.toList po)      go r []       = Just r@@ -276,7 +275,7 @@   go wqo ((f, g) : xs) | Just r  <- getRelation wqo0 g f                        , wqo'    <- get wqo $ insert wqo (g, f, r)                        = go wqo' xs-  go wqo (_ : xs)      | otherwise = go wqo xs+  go wqo (_ : xs)       = go wqo xs  {-# INLINE insertMaybe #-} {-# SPECIALISE insertMaybe :: WQO Op -> (Op, Op, QORelation) -> Maybe (WQO Op) #-}@@ -291,13 +290,13 @@ {-# SPECIALISE insert :: WQO Op -> (Op, Op, QORelation) -> ExtendOrderingResult Op #-} insert :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> ExtendOrderingResult a insert _   (f, g, QGT)  | f == g = Contradicts-insert wqo (f, g, r)    | Just r' <- getRelation wqo f g +insert wqo (f, g, r)    | Just r' <- getRelation wqo f g                         = if r == r' then AlreadyImplied else Contradicts insert wqo (f, g, _)    | isJust $ getRelation wqo g f = Contradicts  insert wqo@(WQO ecs po) (f, g, QEQ) = ValidExtension $     case getEquivalenceClasses wqo f g of-        (Nothing, Nothing) -> +        (Nothing, Nothing) ->             let                 ecs' = S.insert (EC.fromList [f, g]) ecs             in@@ -308,7 +307,7 @@  insert wqo@(WQO ecs po) (f, g, QGT) = ValidExtension $     case getEquivalenceClasses wqo f g of-        (Nothing, Nothing) -> +        (Nothing, Nothing) ->             let                 f'       = EC.singleton f                 g'       = EC.singleton g@@ -316,7 +315,7 @@                 Just po' = PO.insert po f' g'             in                 WQO ecs' po'-        (Just ec, Nothing)   -> +        (Just ec, Nothing)   ->             let                 g'       = EC.singleton g                 ecs'     = S.insert g' ecs@@ -324,14 +323,14 @@             in                 WQO ecs' po' -        (Nothing, Just ec) -> +        (Nothing, Just ec) ->             let                 f'       = EC.singleton f                 ecs'     = S.insert f' ecs                 Just po' = PO.insert po f' ec             in                 WQO ecs' po'-        (Just ec1, Just ec2) -> +        (Just ec1, Just ec2) ->             WQO ecs (PO.insertUnsafe po ec1 ec2)  -- | Generates all the possible orderings of the elements in the given set.

@@ -12,7 +12,7 @@ import qualified Data.Map as M  termOps :: RuntimeTerm -> [Op]-termOps (App f xs) = f:(concatMap termOps xs)+termOps (App f xs) = f:concatMap termOps xs  arityConstraints :: RuntimeTerm -> SMTExpr Bool arityConstraints t = toExpr $ go M.empty t where@@ -22,7 +22,7 @@   go m (App f ts)  = foldl go (M.insert f 0 m) ts    toExpr m = And $ map toConstraint (M.toList m)-  toConstraint (sym, n) = toSMT sym `smtGTE` (Const n)+  toConstraint (sym, n) = toSMT sym `smtGTE` Const n   -- | @kboGTE t u@ returns the SMT expression describing constraints

@@ -1,11 +1,11 @@-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE DeriveAnyClass #-}++ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE ImplicitParams #-} +++ module Language.REST.LPO (lpo, lpoStrict) where  import Prelude hiding (EQ, GT, lex)@@ -50,7 +50,7 @@ lpo' False oc EQ cs (App f ts) (App g us) =   let     cs'  = intersect oc cs (singleton oc $ f =. g)-    subs = map (uncurry $ lpo' False oc EQ cs') (zip ts us)+    subs = zipWith (lpo' False oc EQ cs') ts us   in     intersectAll oc (cs' : subs) @@ -74,12 +74,12 @@     case3 =       if strict && f /= g       then unsatisfiable oc-      else intersectAll oc ([tDominatesUs, (lex oc (r == GT) cs (lpo' strict) ts us)] ++ symEQ) where-        symEQ = if f == g then [] else [singleton oc (f =. g)]+      else intersectAll oc ([tDominatesUs, lex oc (r == GT) cs (lpo' strict) ts us] ++ symEQ) where+        symEQ = [singleton oc (f =. g) | f /= g]       tDominatesUs = intersectAll oc (map go us) where-      go ui = lpo' strict oc GT cs t ui+      go = lpo' strict oc GT cs t   -- | Constraint generator for a quasi-order extension to the Lexicographic path ordering

@@ -23,7 +23,7 @@   where     isSat'  c             = return $ c >= 0     refine' c _ _         = c - 1-    union'  c c'          = max c c'+    union'                = max     notStrongerThan' c c' = return $ c >= c'  -- | @contramap f oca@ transforms an OCA of terms of type @a@ terms of type @b@,

@@ -1,5 +1,4 @@ {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE ImplicitParams #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -32,7 +31,7 @@   }   where     isSat' :: impl base -> m Bool-    isSat' aoc = OC.isSatisfiable oc aoc+    isSat' = OC.isSatisfiable oc      top' :: impl base     top' = OC.noConstraints oc

@@ -39,7 +39,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 _ | showRejects pp == HideRejects = S.empty-rejectedNodes gt pp p@(_steps, (PathTerm {rejected})) = S.fromList $ map go (HS.toList rejected)+rejectedNodes gt pp p@(_steps, PathTerm {rejected}) = S.fromList $ map go (HS.toList rejected)     where         go :: (term, rule) -> Node         go (rejTerm, _r) = Node (rejNodeID gt p rejTerm) (printTerm pp rejTerm) "dashed" "red"@@ -62,7 +62,7 @@  toEdges :: forall rule term a . (Hashable rule, Hashable term, Hashable a) =>   GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Edge-toEdges gt pp path = allRej `S.union` (S.fromList $ map toEdge (zip subs (tail subs)))+toEdges gt pp path = allRej `S.union` S.fromList (zipWith (curry toEdge) subs (tail subs))     where         subs = subPaths path @@ -86,7 +86,7 @@         toEdge (p0, p1@(ts, _)) =             let                 step        = last ts-                color       = if (fromPLE step) then "brown" else "darkgreen"+                color       = if fromPLE step then "brown" else "darkgreen"                 esubLabel    = printOrd pp (ordering step)                 startNodeID = nodeID (endNode gt pp p0)                 endNodeID   = nodeID (endNode gt pp p1)

@@ -3,7 +3,6 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ImplicitParams #-}  -- | This module contains the implementation of the Recursive Path Quasi-Ordering,@@ -47,7 +46,7 @@ isSubtermOf :: RuntimeTerm -> RuntimeTerm -> Bool isSubtermOf t u@(App _ us) = t == u || any (t `isSubtermOf`) (MS.distinctElems us) -type CacheKey oc = ((oc Op), Relation, RuntimeTerm, RuntimeTerm)+type CacheKey oc = (oc Op, Relation, RuntimeTerm, RuntimeTerm)  type Cache oc = M.HashMap (CacheKey oc) (oc Op) @@ -95,7 +94,7 @@ rpo' oc r cs t@(App f ts) u@(App g us) = incDepth result   where     cs'    = noConstraints oc-    result = cached (cs, r, t, u) $ (intersect oc cs <$> result')+    result = cached (cs, r, t, u) (intersect oc cs <$> result')     result' = cached (cs', r, t, u) $       if r == EQ       then rpoMul oc r (addConstraint oc (f =. g) cs') ts us@@ -122,7 +121,7 @@   -> RT.RuntimeTerm   -> RT.RuntimeTerm   -> Identity (oc Op)-rpoGTE' impl oc t u = rpo impl GTE oc t u+rpoGTE' impl = rpo impl GTE   -- Non symbolic version

@@ -1,8 +1,8 @@-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE DeriveAnyClass #-}++ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE ImplicitParams #-}+ {-# LANGUAGE NamedFieldPuns #-} {-# OPTIONS_GHC -Wno-error=deprecations #-} @@ -97,7 +97,7 @@   , RESTResult rtype)   => RESTParams m rule term oc rtype   -> term-  -> m ((rtype rule term oc), Maybe (Path rule term oc))+  -> m (rtype rule term oc, Maybe (Path rule term oc)) rest RESTParams{re,ru,ocImpl,workStrategy,initRes,target,etStrategy} t =   rest' (RESTState initRes [([], PathTerm t S.empty)] initET Nothing)   where@@ -141,8 +141,8 @@               t'  <- ListT $ S.toList <$> apply ptTerm r               return (t', r) -        accepted :: (S.HashSet (term, rule)) -> m (M.HashMap term oc)-        accepted userRWs = M.fromList <$> (runListT $ do+        accepted :: S.HashSet (term, rule) -> m (M.HashMap term oc)+        accepted userRWs = M.fromList <$> runListT (do           t' <- liftSet $ S.map fst userRWs           guard $ L.notElem t' tsTerms           let ord = refine ocImpl lastOrdering ptTerm t'

@@ -38,10 +38,10 @@ -- 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 :: RuntimeTerm -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)] subTerms t@(App f ts) = (t, id) : concatMap st [0..length ts - 1]   where-    st :: Int -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]+    st :: Int -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]     st i =       let         ti = ts !! i

@@ -6,10 +6,10 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE MultiParamTypeClasses #-}+ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-}+ {-# LANGUAGE UndecidableInstances #-}  -- | This module contains functionality for creating SMTLIB expressions and interacting@@ -142,8 +142,8 @@   go _ (And [])         = "⊤"   go p (And ts)         = eparens p $ T.intercalate " ∧ " $ map (go (not p)) ts   go p (Add ts)         = eparens p $ T.intercalate " + " $ map (go (not p)) ts-  go p (GTE t u)        = eparens p $ T.intercalate " ≥ " $ map (go True) $ [t, u]-  go p (Greater t u)    = eparens p $ T.intercalate " > " $ map (go True) $ [t, u]+  go p (GTE t u)        = eparens p $ T.intercalate " ≥ " $ map (go True) [t, u]+  go p (Greater t u)    = eparens p $ T.intercalate " > " $ map (go True) [t, u]   go _ (Var (SMTVar v)) = v   go _ (Const c)        = T.pack (show c)   go _ _e               = undefined@@ -186,10 +186,10 @@ -- | `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+smtGTE t u  = GTE t u  app :: T.Text -> [SMTExpr a] -> T.Text-app op trms = T.concat $ ["(", op, " ", (T.intercalate " " (map exprString trms)), ")"]+app op trms = T.concat ["(", op, " ", T.intercalate " " (map exprString trms), ")"]  exprString :: SMTExpr a -> T.Text exprString (And [])           = "true"@@ -207,7 +207,7 @@  commandString :: SMTCommand -> T.Text commandString (SMTAssert expr) = app "assert" [expr]-commandString (DeclareVar var) = T.concat $ ["(declare-const ", var,  " Int)"]+commandString (DeclareVar var) = T.concat ["(declare-const ", var,  " Int)"] commandString CheckSat = "(check-sat)" commandString Push     = "(push)" commandString Pop      = "(pop)"@@ -234,7 +234,7 @@ withZ3 :: MonadIO m => (SolverHandle -> m b) -> m b withZ3 f =   do-    z3     <- liftIO $ spawnZ3+    z3     <- liftIO spawnZ3     result <- f z3     liftIO $ killZ3 z3     return result@@ -263,7 +263,7 @@   return sat   where     sendCommands cmds = do-      hPutStr stdIn $ (T.unpack (T.intercalate "\n" (map commandString cmds))) ++ "\n"+      hPutStr stdIn $ T.unpack (T.intercalate "\n" (map commandString cmds)) ++ "\n"       hFlush stdIn  -- | @checkSat expr@ launches Z3, to checks satisfiability of @expr@, terminating Z3

@@ -1,7 +1,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeSynonymInstances #-}+ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GADTs #-}@@ -50,7 +50,7 @@    replace s | Just (from, to) <- L.find ((`T.isPrefixOf` s) . fst) substs             = T.append to $ T.drop (T.length from) s-  replace s | otherwise = s+  replace s  = s    replaceAll :: MT.MetaTerm -> MT.MetaTerm   replaceAll (MT.Var x)            = MT.Var x@@ -67,9 +67,9 @@   go (MT.RWApp (Op op) xs)       = T.concat [op, "(" , T.intercalate ", " (map go xs) , ")"]    goParens mt | needsParens mt = T.pack $ printf "(%s)" (go mt)-  goParens mt | otherwise      = go mt+  goParens mt       = go mt -  needsParens (MT.RWApp (Op op) _) = op `elem` (map fst infixOps)+  needsParens (MT.RWApp (Op op) _) = op `elem` map fst infixOps   needsParens _                    = False  data Relation = GT | GTE | EQ deriving (Eq, Generic, Hashable)

@@ -62,9 +62,7 @@ #ifdef OPTIMIZE_WQO -- Optimization intersect (Sat t) (Sat u) =-  case WQO.merge t u of-    Just t' -> Sat t'-    Nothing -> Unsat+  maybe Unsat Sat (WQO.merge t u) #endif  intersect (Sat w) v            | w == WQO.empty = v@@ -76,19 +74,19 @@ #ifdef OPTIMIZE_WQO intersect (Sat w1) (Intersect (Sat w2) t2) =   case WQO.merge w1 w2 of-    Just w' -> intersect (Sat w') t2+    Just w' -> Sat w' `intersect` t2     Nothing -> Unsat intersect (Sat w1) (Intersect t2 (Sat w2)) =   case WQO.merge w1 w2 of-    Just w' -> intersect (Sat w') t2+    Just w' -> Sat w' `intersect` t2     Nothing -> Unsat intersect (Intersect t1 (Sat w1)) (Sat w2) =   case WQO.merge w1 w2 of-    Just w' -> intersect t1 (Sat w')+    Just w' -> t1 `intersect` Sat w'     Nothing -> Unsat intersect (Intersect (Sat w1) t1) (Sat w2) =   case WQO.merge w1 w2 of-    Just w' -> intersect t1 (Sat w')+    Just w' -> t1 `intersect` Sat w'     Nothing -> Unsat #endif intersect t1 t2            = Intersect t1 t2@@ -108,7 +106,7 @@ -- | @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+addConstraint o = intersect (Sat o)  notStrongerThan   :: (Eq a, ToSMTVar a Int)@@ -117,10 +115,10 @@   -> SMTExpr Bool notStrongerThan t1 t2 | t1 == t2            = smtTrue notStrongerThan t1 _  | t1 == noConstraints = smtTrue-notStrongerThan t1 t2 | otherwise           = Implies (toSMT t2) (toSMT t1)+notStrongerThan t1 t2            = Implies (toSMT t2) (toSMT t1)  noConstraints :: ConstraintsADT a-noConstraints = Sat (WQO.empty)+noConstraints = Sat WQO.empty  unsatisfiable :: ConstraintsADT a unsatisfiable = Unsat@@ -143,8 +141,8 @@ cached key thunk = do   cache <- gets cs   case M.lookup key cache of-    Just result -> trace'' ("ADT Cache hit") $ return result-    Nothing     -> trace'' ("ADT Cache miss") $ do+    Just result -> trace'' "ADT Cache hit" $ return result+    Nothing     -> trace'' "ADT Cache miss" $ do       result <- trace'' "Do thunk" thunk       trace'' "Done" $ modify (\st -> st{cs = M.insert key result (cs st)})       return result@@ -156,7 +154,7 @@ cached' (lhs, rhs) thunk = do   cache <- gets ms   case M.lookup (lhs, rhs) cache of-    Just result -> trace'' ("WQO Cache hit") $ return result+    Just result -> trace'' "WQO Cache hit" $ return result     Nothing     -> trace'' ("WQO Cache miss" ++ show (lhs, rhs)) $ do       trace'' "Done" $ modify (\st -> st{ms = M.insert (rhs, lhs) thunk $ M.insert (lhs, rhs) thunk (ms st)})       return thunk@@ -181,15 +179,15 @@   c1' <- cached c1 $ getConstraints' c1   if null c1'     then return []-    else (cached c2 $ getConstraints' c2) >>= go c1'+    else cached c2 (getConstraints' c2) >>= go c1'   where       go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a]       go c1' c2' = flatten <$>-        (sequence $ do+        sequence (do           wqo1 <- c1'           wqo2 <- c2'           return (cached' (wqo1, wqo2) $ WQO.merge wqo1 wqo2))-      flatten = concatMap Mb.maybeToList+      flatten = Mb.catMaybes       (c1, c2) =         if cost lhs > cost rhs         then (lhs, rhs)@@ -203,7 +201,7 @@ permits adt wqo = any (`WQO.notStrongerThan` wqo) (getConstraints adt)  isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool-isSatisfiable s = toSMT s+isSatisfiable = toSMT  instance (Eq a, Hashable a,  Show a) => Show (ConstraintsADT a) where   show (Sat w)         = show w@@ -226,3 +224,4 @@   union   unsatisfiable   undefined+

@@ -54,9 +54,9 @@     (Sat c1 t1', Sat c2 t2') ->       let         rest =-          (ADT.intersect (ADT.Sat c1) t2') `ADT.union`-          (ADT.intersect (ADT.Sat c2) t1') `ADT.union`-          (ADT.intersect t1' t2')+          ADT.intersect (ADT.Sat c1) t2' `ADT.union`+          ADT.intersect (ADT.Sat c2) t1' `ADT.union`+          ADT.intersect t1' t2'       in         case WQO.merge c1 c2 of           Just c' -> Sat c' rest@@ -74,7 +74,7 @@  -- | Returns a new instance of 'LazyOC' permitting all WQOs noConstraints :: LazyOC a-noConstraints = Sat (WQO.empty) ADT.Unsat+noConstraints = Sat WQO.empty ADT.Unsat  unsatisfiable :: LazyOC a unsatisfiable = Unsat

@@ -46,7 +46,7 @@ --   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))+newtype StrictOC a = StrictOC (S.Set (WQO a))   deriving (Eq, Ord, Generic, Hashable)  instance (Show a, Eq a, Ord a, Hashable a) => Show (StrictOC a) where@@ -61,7 +61,7 @@ -- | 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))+noConstraints = StrictOC (S.singleton WQO.empty)  unsatisfiable :: StrictOC a unsatisfiable = StrictOC S.empty

@@ -1,10 +1,10 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-}-{-# LANGUAGE ImplicitParams #-}+ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeSynonymInstances #-} + module BagExample (mkBagGraph) where  import Prelude hiding (EQ, GT)@@ -31,7 +31,7 @@ import GHC.Generics (Generic) import           Data.Hashable -data PChar = PChar Char deriving (Eq, Ord, Generic, Hashable)+newtype PChar = PChar Char deriving (Eq, Ord, Generic, Hashable)  instance ToSMTVar PChar Int where   toSMTVar c = SMTVar $ T.pack $ "char_" ++ show c@@ -39,7 +39,7 @@ instance Show PChar where   show (PChar c) = return c -data Bag = Bag String+newtype Bag = Bag String   deriving (Eq, Ord, Generic, Hashable)  instance Show Bag where@@ -62,12 +62,12 @@  instance RewriteRule IO Rewrite Bag where   apply bag1 (Rewrite bag' result) | bag1 == bag' = return result-  apply _ _ | otherwise                           = return S.empty+  apply _ _                            = return S.empty   fromPath :: [String] -> S.HashSet Rewrite fromPath [] = S.empty-fromPath xs = S.fromList $ map go (zip xs (tail xs))+fromPath xs = S.fromList $ zipWith (curry go) xs (tail xs)   where     go :: (String, String) -> Rewrite     go (x, y) = Rewrite (bag x) (S.singleton $ bag y)@@ -80,13 +80,13 @@ start = "AAB"  rules :: S.HashSet Rewrite-rules = fromPaths $+rules = fromPaths   [  start ~> "ACD" ~> "AAAA" ~> "ABDD" ~> []   ,  start ~> "ABD" ~> "AB"  ~> "BBD" ~> []   ]  showBag :: Bag -> String-showBag (Bag bag1) = "{ " ++ (L.intercalate ", " $ map return bag1) ++ " }"+showBag (Bag bag1) = "{ " ++ L.intercalate ", " (map return bag1) ++ " }"  showRule :: Rewrite -> String showRule _ = ""

@@ -21,6 +21,6 @@       [           x #+ zero'    ~> x         , zero'    #+ x ~> x-        , (neg x) #+ x  ~> zero'+        , neg x #+ x  ~> zero'         , (x #+ y) #+ v ~> x #+ (y #+ v)       ]

@@ -35,6 +35,6 @@  userRWs :: S.HashSet Rewrite userRWs = S.fromList [-    reverse (xs .++ ys) ~> (reverse ys) .++ (reverse xs)-  , (reverse ys) .++ (reverse xs) ~> reverse (xs .++ ys)+    reverse (xs .++ ys) ~> reverse ys .++ reverse xs+  , reverse ys .++ reverse xs ~> reverse (xs .++ ys)   ]

@@ -1,4 +1,4 @@-{-# LANGUAGE ImplicitParams #-}+ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} @@ -20,7 +20,7 @@ import Language.REST.Internal.WorkStrategy import DSL import Nat-import Set as Set+import Set import qualified Multiset as MS import NonTerm as NT import qualified Lists as Li@@ -77,7 +77,7 @@       do         mapM_ (explain (refine impl (top impl))) pairs         printf "Result:\n%s\n" (show $ orient impl ts)-        (isSatisfiable SC.strictOC (orient impl ts)) >>= print+        isSatisfiable SC.strictOC (orient impl ts) >>= print     where       impl :: OCAlgebra (SC.StrictOC Op) RuntimeTerm Identity       impl = lift SC.strictOC lpo@@ -142,9 +142,9 @@ mkRESTGraph' impl evalRWs0 userRWs0 name term0 params =   do     let pr (Rewrite t u _) = printf "%s → %s" (pp t) (pp u)-    liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList userRWs0-    liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList evalRWs0-    start <- liftIO $ getCurrentTime+    liftIO $ mapM_ (putStrLn . pr) $ S.toList userRWs0+    liftIO $ mapM_ (putStrLn . pr) $ S.toList evalRWs0+    start <- liftIO getCurrentTime     (PathsResult paths, targetPath) <- rest       RESTParams         { re           = evalRWs0@@ -155,7 +155,7 @@         , initRes      = pathsResult         , etStrategy   = if gUseETOpt params then ExploreWhenNeeded else ExploreAlways         } (parseTerm term0)-    end <- liftIO $ getCurrentTime+    end <- liftIO getCurrentTime     liftIO $ printf "REST run completed, in %s\n" $ show $ diffUTCTime end start     liftIO $ putStrLn "Drawing graph"     let showCons = if gShowConstraints params then show else const ""@@ -189,5 +189,5 @@ main :: IO () main = do   mkRESTGraph RPO S.empty (S.insert (s1 /\ s0 ~> emptyset) challengeRulesNoCommute) "fig4" "f(intersect(union(s₀,s₁), s₀))" (withNoETOpt defaultParams)-  mkRESTGraph RPO S.empty (S.fromList $ [x #+ y ~> y #+ x] ++ ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-noopt" "a + (b + a)" (withNoETOpt defaultParams)-  mkRESTGraph RPO S.empty (S.fromList $ [x #+ y ~> y #+ x] ++ ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-opt" "a + (b + a)" defaultParams+  mkRESTGraph RPO S.empty (S.fromList $ (x #+ y ~> y #+ x) : ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-noopt" "a + (b + a)" (withNoETOpt defaultParams)+  mkRESTGraph RPO S.empty (S.fromList $ (x #+ y ~> y #+ x) : ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-opt" "a + (b + a)" defaultParams

@@ -37,17 +37,17 @@ expandM xs0 = multisetOf xs0 ~> ite (isEmpty xs0) empty (singleton (hd xs0) \/ multisetOf (tl xs0))  userRWs :: S.HashSet Rewrite-userRWs = S.fromList $+userRWs = S.fromList   [     commutes (\/) `named` "mpComm"   , assocL (\/) `named` "mpAssoc"   , assocR (\/) `named` "mpAssoc"-  , (singleton x) \/ (multisetOf y) ~> multisetOf (cons x y)+  , singleton x \/ multisetOf y ~> multisetOf (cons x y)   ]  evalRWs :: S.HashSet Rewrite evalRWs = S.fromList-  [ multisetOf (cons x y) ~> (singleton x) \/ (multisetOf y)+  [ multisetOf (cons x y) ~> singleton x \/ multisetOf y   , expandM xs   , expandM ys   ]

@@ -31,7 +31,7 @@ tests :: [(String, Bool)] tests = [     ("Constraints",-     (SC.noConstraints /=-     (runIdentity $ ms SC.noConstraints (M.fromList "bc") (M.fromList "aa"))))+     SC.noConstraints /=+     runIdentity (ms SC.noConstraints (M.fromList "bc") (M.fromList "aa")))   , ("Unsat", SC.isUnsatisfiable $ runIdentity unsat)   ]

@@ -16,7 +16,7 @@ d' x1 = RWApp (Op "d") [x1]  userRWs :: S.HashSet Rewrite-userRWs = S.fromList $+userRWs = S.fromList   [     a' (b' x) ~> a' (d' x)   , d' (b' x) ~> b' (d' x)

@@ -22,11 +22,11 @@   ) ]         where -        Just wqo = mergeAll [ ("cons" =. "z")-                , ("g" =. "nil")-                , ("h" =. "s")-                , ("cons" >. "g")-                , ("cons" >. "h")-                , ("h" >. "f")-                , ("h" >. "g")+        Just wqo = mergeAll [ "cons" =. "z"+                , "g" =. "nil"+                , "h" =. "s"+                , "cons" >. "g"+                , "cons" >. "h"+                , "h" >. "f"+                , "h" >. "g"                 ]

@@ -54,7 +54,7 @@       let po' = fromMaybe po $ PO.insert po f g       go po' (n - 1) -gen_wqo_steps :: Gen ([(Op, Op, WQO.QORelation)])+gen_wqo_steps :: Gen [(Op, Op, WQO.QORelation)] gen_wqo_steps =   do     numOps <- choose (0, 10)@@ -83,7 +83,7 @@   where     go :: Int -> Gen RuntimeTerm     go sz = do-      (op, arity) <- oneof $ map return $ (filter ((<= sz) . snd) syms)+      (op, arity) <- oneof $ map return $ filter ((<= sz) . snd) syms       args        <- vectorOf arity (go (sz `div` (arity + 1)))       return $ App (Op op) args @@ -134,7 +134,7 @@     ordering    = Mb.fromJust (OC.getOrdering impl constraints)  prop_permits :: [(Op, Op, WQO.QORelation)] -> Bool-prop_permits steps = SC.permits (SC.noConstraints) (toWQO steps)+prop_permits steps = SC.permits SC.noConstraints (toWQO steps)  -- Should fail -- If this prop was true, we'd only ever need to check each term once

@@ -47,7 +47,7 @@   :: (?impl::WQOConstraints impl m, Show (impl Op), Eq (impl Op), Hashable (impl Op))   => [RuntimeTerm]   -> impl Op-rpoSeq xs = go (OC.noConstraints ?impl) xs where+rpoSeq = go (OC.noConstraints ?impl) where   go c (t:u:_xss) = OC.intersect ?impl c (rpoGTE t u)   go c _        = c @@ -59,7 +59,7 @@     g = Op "g"     h = Op "h"   in-    [ ("RPO1",   return $ (rpoGTE "f(z)" "g(s(z))")+    [ ("RPO1",   return $ rpoGTE "f(z)" "g(s(z))"               == OC.intersect ?impl (OC.singleton ?impl (f >. g)) (OC.singleton ?impl (f >. s)))     , ("RPO2", isUnsatisfiable ?impl $          OC.intersect ?impl@@ -73,8 +73,8 @@     , ("SynGTE", return $ synGTE OpOrdering.empty (App s [App s [App g [App (Op "+") [App h [App s [App z []]],App z []],App s [App s [App g [App z [],App z []]]]]]]) (App z []))     , ("SynGTE2",         return $ synGTE (Mb.fromJust $ mergeAll [-          ("cons" >. g)-        , (f >. s)-        , (h >. g)-        , (h >. "nil")]) "s(cons(h(h(z)), f(nil, nil, z)))"  "g(z, cons(g(nil, nil), s(s(z))))")+          "cons" >. g+        , f >. s+        , h >. g+        , h >. "nil"]) "s(cons(h(h(z)), f(nil, nil, z)))"  "g(z, cons(g(nil, nil), s(s(z))))")     ]

@@ -13,11 +13,11 @@     ("permits", permits noConstraints wqo)   , ("permits2", permits noConstraints $ fromJust $ parseOO "+ = f = nil = s ∧ + > g ∧ + > h ∧ cons > + ∧ cons > g")   ] where-  Just wqo = mergeAll [ ("cons" =. "z")-                      , ("g" =. "nil")-                      , ("h" =. "s")-                      , ("cons" >. "g")-                      , ("cons" >. "h")-                      , ("h" >. "f")-                      , ("h" >. "g")+  Just wqo = mergeAll [ "cons" =. "z"+                      , "g" =. "nil"+                      , "h" =. "s"+                      , "cons" >. "g"+                      , "cons" >. "h"+                      , "h" >. "f"+                      , "h" >. "g"                       ]

@@ -1,4 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-}@@ -8,22 +9,25 @@  import qualified Data.List as L import Data.Hashable+#if MIN_VERSION_mtl(2,3,0)+import Control.Monad (guard)+#endif import Control.Monad.Identity import qualified Arith as A  import qualified Data.HashMap.Strict as M-import qualified ExploredTerms as ExploredTerms+import qualified ExploredTerms import OpOrdering import DSL-import WQO as WQO-import MultisetOrder as MultisetOrder+import WQO+import MultisetOrder import Nat-import RPO as RPO-import KBO as KBO-import StrictOC as StrictOC-import LazyOC as LazyOC-import SMT as SMT-import qualified QuickCheckTests as QuickCheckTests+import RPO+import KBO+import StrictOC+import LazyOC+import SMT+import qualified QuickCheckTests import System.IO  import Language.REST.ExploredTerms@@ -56,13 +60,13 @@ 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)+diverges impl ts = not <$> isSat impl (orient impl ts)  rewrites :: (Show oc, Hashable oc, Eq oc)   => OCAlgebra oc RuntimeTerm IO   -> S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm) rewrites impl evalRWs userRWs t0 =-  resultTerms <$> fst <$> rest+  resultTerms . fst <$> rest     RESTParams       { re           = evalRWs       , ru           = userRWs@@ -104,9 +108,9 @@ orderingTests :: (Hashable (oc Op), Show (oc Op), Ord (oc Op)) => (?impl :: WQOConstraints oc IO) => [(String, IO Bool)] orderingTests =   [-    ("simple1", return $ not $ (rpoGTE "f(t1)" "g(t2)") `permits'` (t1Op =. t2Op))-  , ("simple2", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op =. t2Op)))-  , ("simple3", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op >. t2Op)))+    ("simple1", return $ not $ rpoGTE "f(t1)" "g(t2)" `permits'` (t1Op =. t2Op))+  , ("simple2", return $ rpoGTE "f(t1)" "g(t2)" `permits'` Mb.fromJust (merge (f >. g) (t1Op =. t2Op)))+  , ("simple3", return $ rpoGTE "f(t1)" "g(t2)" `permits'` Mb.fromJust (merge (f >. g) (t1Op >. t2Op)))   , ("subterm", return $ rpoGTE "f(g)" "f" == noConstraints ?impl)   , ("intersect", OC.isUnsatisfiable ?impl $ OC.intersect ?impl (OC.singleton ?impl (f  >. g)) (OC.singleton ?impl (g >. f)))   ]@@ -119,8 +123,8 @@   -> RuntimeTerm -> RuntimeTerm -> IO Bool proveEQ impl evalRWs userRWs have want =   do-    rw1 <- (rewrites impl evalRWs userRWs have)-    rw2 <- (rewrites impl evalRWs userRWs want)+    rw1 <- rewrites impl evalRWs userRWs have+    rw2 <- rewrites impl evalRWs userRWs want     return $ not $ disjoint rw1 rw2   where     disjoint s1 s2 = S.null $ s1 `S.intersection` s2@@ -137,15 +141,13 @@ arithTests impl =   [     ("Contains", return $ contains (intToTerm 2) (intToTerm 1))-  , ("Diverge", not <$> (diverges impl [ (intToTerm 2) .+ t1-                               , (intToTerm 1) .+ t1-                               ]-                    ))-  , ("Diverge3", not <$> (diverges impl [ (t1 .+ t2) .+ t3+  , ("Diverge", not <$> diverges impl [ intToTerm 2 .+ t1+                               , intToTerm 1 .+ t1+                               ])+  , ("Diverge3", not <$> diverges impl [ (t1 .+ t2) .+ t3                                , t1 .+ (t2 .+ t3)                                , (t2 .+ t3) .+ t1-                               ]-                    ))+                               ])   , ("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))@@ -184,7 +186,7 @@     termTest2 = proveEQ impl evalRWs userRWs (App f1 [zero]) (App g1 [zero])       where         evalRWs = S.union termEvalRWs A.evalRWs-        userRWs = S.insert (MT.RWApp f1 [x] ~> MT.RWApp g1 [(suc' (suc' x))]) A.userRWs+        userRWs = S.insert (MT.RWApp f1 [x] ~> MT.RWApp g1 [suc' (suc' x)]) A.userRWs         termEvalRWs = S.fromList           [  MT.RWApp f1 [suc' x] ~> MT.RWApp g1 [suc' x]           ,  MT.RWApp f1 [zero']  ~> zero'@@ -201,7 +203,7 @@ completeTests impl =   [ ("CompleteDiverges", not <$> diverges impl [App start [], App mid [], App finish []])   , ("Complete1"     , eq (App start []) (App finish []))-  , ("EvalComplete2" , (== (App finish [])) <$> eval completeUserRWs (App start' [App s1 []]) )+  , ("EvalComplete2" , (== App finish []) <$> eval completeUserRWs (App start' [App s1 []]) )   , ("Complete2"     , eq (App start' [App s1 []]) (App finish []))   ]   where

@@ -1,6 +1,7 @@ module WQO where  import Language.REST.Internal.WQO as WQO+import Data.Maybe (isNothing)  basicInvalid :: Maybe (WQO Char) basicInvalid = do@@ -14,5 +15,5 @@     ValidExtension fgyz = insert fg ("y", "z", QGT)   in     [ ("NotStrongerThan", fg `notStrongerThan` fgyz)-    , ("RejectInvalid", basicInvalid == Nothing)+    , ("RejectInvalid", isNothing basicInvalid)     ]

@@ -24,11 +24,11 @@ evalRWs =     S.fromList       [-        (suc' x) <# (suc' y) ~> x <# y-      , (suc' x) #+ y ~> suc' (x #+ y)+        suc' x <# suc' y ~> x <# y+      , suc' x #+ y ~> suc' (x #+ y)       , zero'    #+ x ~> x -      , (suc' x) #* y ~> y #+ (x #* y)+      , suc' x #* y ~> y #+ (x #* y)       , zero'     #* y ~> zero'        , ack' zero' x           ~> suc' x@@ -46,7 +46,7 @@       , x #* y        ~> y #* x        , (x #+ y) #* v ~> (x #* v) #+ (y #* v)-      , (neg x) #+ x ~> zero'+      , neg x #+ x ~> zero'       -- , (x #* v) #+ (y #* v) ~> (x #+ y) #* v        --  , x ~> x #+ zero'

@@ -13,7 +13,7 @@ import GHC.Generics (Generic) import qualified Data.Set as S -data ConcreteOC = ConcreteOC (S.Set (WQO.WQO Op))+newtype ConcreteOC = ConcreteOC (S.Set (WQO.WQO Op))   deriving (Eq, Ord, Generic, Hashable)  instance Show ConcreteOC where

@@ -28,23 +28,20 @@  toLH _ (App op [])   = opToLH op toLH parens (App op args) =-  withParens parens $ printf "%s %s" (opToLH op) (L.intercalate " " $ map (toLH True) args)+  withParens parens $ printf "%s %s" (opToLH op) (unwords $ map (toLH True) args)  toProof :: Path Rewrite RuntimeTerm a -> String-toProof (steps, PathTerm result _) = "    " ++ (L.intercalate "\n=== " $ proofSteps ++ [toLH False result]) ++ "\n*** QED"+toProof (steps, PathTerm result _) = "    " ++ L.intercalate "\n=== " (proofSteps ++ [toLH False result]) ++ "\n*** QED"   where     proofSteps :: [String]-    proofSteps = map proofStep $ zip steps [0..]+    proofSteps = zipWith (curry proofStep) steps [0..] -    proofStep ((Step (PathTerm t _) _ _ True), _)     = toLH False t-    proofStep ((Step (PathTerm t _) (Rewrite lhs rhs name) _ False), i) = toLH False t ++ " ? " ++ toLemma lemma+    proofStep (Step (PathTerm t _) _ _ True, _)                       = toLH False t+    proofStep (Step (PathTerm t _) (Rewrite lhs rhs name) _ False, i) = toLH False t ++ " ? " ++ toLemma lemma       where         lemma = go (subTerms t) -        lemmaName =-          case name of-            Just n  -> T.pack n-            Nothing -> "lemma"+        lemmaName = maybe "lemma" T.pack name          toLemma s = toLH False (App (Op lemmaName) (map snd $ L.sort $ M.toList s)) 

@@ -15,7 +15,7 @@   | Replace a [a]   deriving (Show) -data MultisetGE a = MultisetGE [Replace a] deriving (Show)+newtype MultisetGE a = MultisetGE [Replace a] deriving (Show)  type GTE a = a -> a -> Bool @@ -31,14 +31,14 @@      go :: [Replace a] -> [a] -> [a] -> Maybe (MultisetGE a)     go rs (t : ts) us | Just u <- L.find (equiv t) us-      = go ((ReplaceOne t u):rs) ts (L.delete u us)+      = go (ReplaceOne t u:rs) ts (L.delete u us) -    go rs (t : ts) us | otherwise =+    go rs (t : ts) us  =         let           (lts, us') = L.partition (t `gt`)  us         in-          go ((Replace t lts) : rs) ts us'-    go rs ts [] = Just $ MultisetGE $ (map ((flip Replace) []) ts) ++ rs+          go (Replace t lts : rs) ts us'+    go rs ts [] = Just $ MultisetGE $ map (`Replace` []) ts ++ rs     go _  [] _  = Nothing  @@ -78,13 +78,13 @@       from edge == nodeID node || to edge == nodeID node      edges :: S.HashSet Edge-    edges = S.fromList $ topEdges ++ (map snd $ replEdges pairs)+    edges = S.fromList $ topEdges ++ map snd (replEdges pairs)      topEdges = map go (M.toList (fst $ head indexed)) where       go (_, index) =         mkEdge "⊤" (nodeName (index,  0)) -    botNodes = S.fromList $ concatMap Mb.maybeToList $ map fst $ replEdges pairs+    botNodes = S.fromList $ Mb.mapMaybe fst (replEdges pairs)      nodeName :: (Int,  Int) -> String     nodeName (elemIndex,  msIndex) =@@ -92,7 +92,7 @@      replEdges = toEdges Mp.empty -    toEdges :: Mp.HashMap (Int, Int) (Int, Int) -> [IndexedMultisetPair a] -> ([(Maybe Node, Edge)])+    toEdges :: Mp.HashMap (Int, Int) (Int, Int) -> [IndexedMultisetPair a] -> [(Maybe Node, Edge)]     toEdges _ [] = []     toEdges mp (((ts, tsIndex), (us, usIndex)) : mss) =         concatMap redges repls ++ toEdges mp' mss@@ -100,9 +100,7 @@         Just (MultisetGE repls) = multisetGE (\t u -> gte (fst t) (fst u)) ts us          lookupTIndex :: Int -> (Int, Int)-        lookupTIndex tindex = case Mp.lookup (tindex, tsIndex) mp of-          Just t  -> t-          Nothing -> (tindex, tsIndex)+        lookupTIndex tindex = Mb.fromMaybe (tindex, tsIndex) (Mp.lookup (tindex, tsIndex) mp)          mp' = go mp repls where           go mpi [] = mpi

@@ -46,7 +46,7 @@                   ] showInt)   where     showInt :: MT.MetaTerm -> Maybe Text-    showInt t = fmap (pack . show) $ termToInt t+    showInt t = pack . show <$> termToInt t  op :: GenParser Char st Op op = fmap (Op . pack) (many (alphaNum <|> char '\''))

@@ -24,7 +24,7 @@ isSubset mt1 mt2 = mt1 \/ mt2 ~> mt2  userRWs :: S.HashSet Rewrite-userRWs = S.union A.evalRWs $ S.fromList $+userRWs = S.union A.evalRWs $ S.fromList   [     distribL (/\) (\/)   , distribR (/\) (\/)