diff --git a/src/Data/Rewriting/Rule/Ops.hs b/src/Data/Rewriting/Rule/Ops.hs --- a/src/Data/Rewriting/Rule/Ops.hs +++ b/src/Data/Rewriting/Rule/Ops.hs @@ -11,6 +11,7 @@ varsDL, left, right, + rename, -- * Predicates on Rules both, isLinear, isLeftLinear, isRightLinear, @@ -44,6 +45,15 @@ -- | Apply a function to the rhs of a rule. right :: (Term f v -> a) -> Rule f v -> a right f = f . rhs + + +-- | Lifting of 'Term.rename' to 'Rule': renames left- and +-- right-hand sides. +-- >>> rename (+ 1) $ Rule {lhs = (Fun 'f' [Var 1, Fun 'g' [Var 2]]), rhs = Fun 'g' [Var 1]} +-- Rule {lhs = (Fun 'f' [Var 2, Fun 'g' [Var 3]]), rhs = Fun 'g' [Var 2]} +rename :: (v -> v') -> Rule f v -> Rule f v' +rename f rl = Rule (left (Term.rename f) rl) (right (Term.rename f) rl) + -- | Lifting of 'Term.funs' to 'Rule': returns the list of function symbols -- in left- and right-hand sides. diff --git a/src/Data/Rewriting/Substitution/Ops.hs b/src/Data/Rewriting/Substitution/Ops.hs --- a/src/Data/Rewriting/Substitution/Ops.hs +++ b/src/Data/Rewriting/Substitution/Ops.hs @@ -5,6 +5,8 @@ module Data.Rewriting.Substitution.Ops ( apply, + applyRule, + applyCtxt, gApply, compose, merge, @@ -13,6 +15,8 @@ import Data.Rewriting.Substitution.Type import qualified Data.Rewriting.Term.Type as Term import Data.Rewriting.Term.Type (Term (..)) +import Data.Rewriting.Rule.Type (Rule (..)) +import Data.Rewriting.Context.Type (Ctxt (..)) import qualified Data.Map as M import Control.Monad import Control.Applicative @@ -23,6 +27,17 @@ apply subst = Term.fold var fun where var v = M.findWithDefault (Var v) v (toMap subst) fun = Fun + +-- | Liftting of 'apply' to rules: applies the given substitution to left- and right-hand side. +applyRule :: (Ord v) => Subst f v -> Rule f v -> Rule f v +applyRule subst rl = Rule (apply subst (lhs rl)) (apply subst (rhs rl)) + +-- | Liftting of 'apply' to contexts. +applyCtxt :: Ord v => Subst f v -> Ctxt f v -> Ctxt f v +applyCtxt _ Hole = Hole +applyCtxt subst (Ctxt f ts1 ctxt ts2) = + Ctxt f (map (apply subst) ts1) (applyCtxt subst ctxt) (map (apply subst) ts2) + -- | Apply a substitution, assuming that it's total. If the term contains -- a variable not defined by the substitution, return 'Nothing'. diff --git a/src/Data/Rewriting/Term/Ops.hs b/src/Data/Rewriting/Term/Ops.hs --- a/src/Data/Rewriting/Term/Ops.hs +++ b/src/Data/Rewriting/Term/Ops.hs @@ -9,9 +9,13 @@ funsDL, vars, varsDL, + root, withArity, subtermAt, + properSubterms, + subterms, replaceAt, + rename, -- * Predicates on Terms isVar, isFun, @@ -43,6 +47,20 @@ subtermAt (Fun _ ts) (p:ps) | p >= 0 && p < length ts = subtermAt (ts !! p) ps subtermAt _ _ = Nothing +-- | Return the list of all proper subterms. +-- +-- >>> properSubterms (Fun 'g' [Fun 'f' [Var 1], Fun 'f' [Var 1]]) +-- [Fun 'f' [Var 1],Var 1,Fun 'f' [Var 1],Var 1] +properSubterms :: Term f v -> [Term f v] +properSubterms (Var _) = [] +properSubterms (Fun _ ts) = concatMap subterms ts + +-- | Return the list of all subterm. +-- +-- prop> subterms t = t : properSubterms t +subterms :: Term f v -> [Term f v] +subterms t = t : properSubterms t + -- NOTE: replaceAt and Context.ofTerm have the same recusion structure; is -- there a nice higher-order function to abstract from it? @@ -69,6 +87,18 @@ varsDL :: Term f v -> [v] -> [v] varsDL = Term.fold (:) (const $ foldr (.) id) + +-- | Return the root symbol of the given term. +-- +-- >>> root (Fun 'f' [Var 1, Fun 'g' []]) +-- Right 'f' +-- +-- >>> root (Var 1) +-- Left 1 +root :: Term f v -> Either v f +root (Fun f _) = Right f +root (Var v) = Left v + -- | Return the list of all function symbols in the term, from left to right. -- -- >>> funs (Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]]) @@ -78,7 +108,6 @@ -- | Difference List version of 'funs'. -- We have @funsDL t vs = funs t ++ vs@. - funsDL :: Term f v -> [f] -> [f] funsDL = Term.fold (const id) (\f xs -> (f:) . foldr (.) id xs) @@ -108,3 +137,10 @@ -- | Check whether a term is a variant of another. isVariantOf :: (Eq f, Ord v, Ord v') => Term f v -> Term f v' -> Bool isVariantOf t u = isInstanceOf t u && isInstanceOf u t + +-- | Rename the variables in a term. +-- +-- >>> rename (+ 1) (Fun 'f' [Var 1, Fun 'g' [Var 2]]) +-- (Fun 'f' [Var 2, Fun 'g' [Var 3]]) +rename :: (v -> v') -> Term f v -> Term f v' +rename = Term.map id diff --git a/term-rewriting.cabal b/term-rewriting.cabal --- a/term-rewriting.cabal +++ b/term-rewriting.cabal @@ -1,10 +1,10 @@ name: term-rewriting -version: 0.1 +version: 0.1.1 stability: experimental author: Martin Avanzini, Bertram Felgenhauer, - Christian Sternagel -homepage: http://cl-informatik.uibk.ac.at/software/haskell-rewriting/ + Christian Sternagel, + Ilya Epifanov maintainer: haskell-rewriting@informatik.uibk.ac.at license: MIT license-file: LICENSE @@ -16,7 +16,7 @@ This library provides basic data types and functionality for first order term rewriting. build-type: Simple -cabal-version: >= 1.6 +cabal-version: >= 1.8 source-repository head type: git @@ -64,10 +64,21 @@ multiset >= 0.2 && < 0.3, parsec >= 3 && < 3.2, union-find-array >= 0.1 && < 0.2, - array >= 0.3 && < 0.5, + array >= 0.3 && < 0.6, ansi-wl-pprint >= 0.6 && < 0.7, - mtl >= 1.1 && < 2.2, + mtl >= 1.1 && < 2.3, base >= 4 && < 5 extensions: TypeSynonymInstances BangPatterns + +test-suite test + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Main.hs + build-depends: + base >= 4 && < 5, + term-rewriting, + containers >= 0.3 && < 0.6, + HUnit >= 1.2 && < 1.3, + QuickCheck >= 2.6 && < 2.7 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,52 @@ +-- This file is part of the 'term-rewriting' library. It is licensed +-- under an MIT license. See the accompanying 'LICENSE' file for details. +-- +-- Authors: Bertram Felgenhauer + +-- Main test driver. + +module Main (main) where + +import qualified Pos +import qualified Term +import qualified Rule +import qualified CriticalPair +import qualified Substitution + +import Test.QuickCheck +import Test.HUnit +import Control.Monad +import System.IO + +properties :: [(String, Property)] +properties = [ + ("Pos.propParallelTo", property Pos.propParallelTo), + ("Term.propReplaceAt1", property Term.propReplaceAt1), + ("Term.propReplaceAt2", property Term.propReplaceAt2), + ("Rule.propLeftRightLinearDual", property Rule.propLeftRightLinearDual), + ("Rule.propCollapsingExpandingDual", property Rule.propCollapsingExpandingDual), + ("Rule.propErasingCreatingDual", property Rule.propErasingCreatingDual), + ("Rule.propLinear", property Rule.propLinear), + ("Rule.propValid", property Rule.propValid), + ("Substitution.propCompose", property Substitution.propCompose), + ("Substitution.propUnify1", property Substitution.propUnify1), + ("Substitution.propUnify2", property Substitution.propUnify2), + ("CriticalPair.propValidCPs'", property CriticalPair.propValidCPs'), + ("CriticalPair.propOuterCPs'", property CriticalPair.propOuterCPs'), + ("CriticalPair.propInnerCPs'", property CriticalPair.propInnerCPs') + ] + +tests :: Test +tests = TestList [ + CriticalPair.tests, + Rule.tests, + TestList []] + +main :: IO () +main = do + forM_ properties $ \(name, prop) -> do + putStrLn $ "- " ++ name + quickCheck prop + putStrLn $ "- HUnit tests" + runTestTT tests + return ()