term-rewriting 0.1 → 0.1.1

raw patch · 5 files changed

+131/−7 lines, 5 filesdep +HUnitdep +QuickCheckdep +term-rewritingdep ~arraydep ~basedep ~mtlPVP ok

version bump matches the API change (PVP)

Dependencies added: HUnit, QuickCheck, term-rewriting

Dependency ranges changed: array, base, mtl

API changes (from Hackage documentation)

Files

• src/Data/Rewriting/Rule/Ops.hs +10/−0
• src/Data/Rewriting/Substitution/Ops.hs +15/−0
• src/Data/Rewriting/Term/Ops.hs +37/−1
• term-rewriting.cabal +17/−6
• test/Main.hs +52/−0

@@ -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.

@@ -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'.

@@ -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 

@@ -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

@@ -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 ()