packages feed

term-rewriting 0.2.1.1 → 0.3

raw patch · 10 files changed

+349/−6 lines, 10 filesdep ~HUnitdep ~QuickCheckdep ~containers

Dependency ranges changed: HUnit, QuickCheck, containers

Files

Changelog view
@@ -1,3 +1,9 @@+version 0.3+	- drop Control.Monad.Error import in Data.Rewriting.Term.Parse+	- fix testsuite+	  * include all modules in source distribution+	  * build fix for recent QuickCheck+ version 0.2.1.1         - Changelog
src/Data/Rewriting/Term/Parse.hs view
@@ -16,7 +16,6 @@ import Data.Rewriting.Utils.Parse (lex, par, ident) import Prelude hiding (lex) import Control.Monad-import Control.Monad.Error () import Data.Rewriting.Term.Type import Text.Parsec hiding (parse) import Text.Parsec.Prim (runP)
term-rewriting.cabal view
@@ -1,5 +1,5 @@ name:          term-rewriting-version:       0.2.1.1+version:       0.3 stability:     experimental author:        Martin Avanzini,                Bertram Felgenhauer,@@ -64,7 +64,7 @@         Data.Rewriting.Utils         Data.Rewriting.Utils.Parse     build-depends:-        containers >= 0.3 && < 0.6,+        containers >= 0.3 && < 0.7,         multiset >= 0.2 && < 0.4,         parsec >= 3.1.6 && < 3.2,         union-find-array >= 0.1 && < 0.2,@@ -80,9 +80,17 @@     type:  exitcode-stdio-1.0     hs-source-dirs: test     main-is: Main.hs+    other-modules:+        Arbitrary+        CriticalPair+        Pos+        Rule+        Samples+        Substitution+        Term     build-depends:         base >= 4 && < 5,         term-rewriting,-        containers >= 0.3 && < 0.6,-        HUnit >= 1.2 && < 1.3,-        QuickCheck >= 2.6 && < 2.7+        containers >= 0.3 && < 0.7,+        HUnit >= 1.2 && < 1.7,+        QuickCheck >= 2.6 && < 2.13
+ test/Arbitrary.hs view
@@ -0,0 +1,88 @@+-- 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++{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}++-- Types and Arbitrary instances for tests.++module Arbitrary (+    Var',+    Fun',+    Term',+    Rule',+    Subst',+) where++import Data.Rewriting.Term (Term (..))+import Data.Rewriting.Rule (Rule (..))+import qualified Data.Rewriting.Rule as Rule+import Data.Rewriting.Substitution (Subst, GSubst)+import qualified Data.Rewriting.Substitution.Type as Subst++import Test.QuickCheck (Arbitrary (..), CoArbitrary (..), (><))+import Test.QuickCheck.Gen+import Control.Applicative+import Control.Monad+import qualified Data.Map as M++newtype Var' = Var' Char+    deriving (Eq, Ord)++newtype Fun' = Fun' Char+    deriving (Eq, Ord)++type Term' = Term Fun' Var'++type Rule' = Rule Fun' Var'++type Subst' = Subst Fun' Var'++instance Show Var' where+    showsPrec p (Var' c) = showsPrec p c++instance Show Fun' where+    showsPrec p (Fun' c) = showsPrec p c++instance Arbitrary Var' where+    arbitrary = Var' <$> growingElements "xyzuvw"++instance CoArbitrary Var' where+    coarbitrary (Var' c) = coarbitrary c++instance Arbitrary Fun' where+    arbitrary = Fun' <$> growingElements "fghijk"++instance CoArbitrary Fun' where+    coarbitrary (Fun' c) = coarbitrary c++constant :: Gen Fun'+constant = Fun' <$> growingElements "abcd"++instance Arbitrary Term' where+    arbitrary = oneof [+        Var <$> arbitrary,+        Fun <$> constant <*> pure [],+        Fun <$> arbitrary <*> args]+      where+        args = sized $ \n -> do+            k <- choose (1, 1 `max` n)+            let n' = if k == 1 then n else 2*n `div` k+            replicateM k (resize n' arbitrary)++instance CoArbitrary Term' where+    coarbitrary (Var x) = variant 0 . coarbitrary x+    coarbitrary (Fun f ts) = variant (-1) . (coarbitrary f >< coarbitrary ts)++instance Arbitrary Rule' where+    arbitrary = (Rule <$> arbitrary <*> arbitrary) `suchThat` Rule.isValid++instance CoArbitrary Rule' where+    coarbitrary (Rule l r) = coarbitrary l >< coarbitrary r++instance Arbitrary Subst' where+    arbitrary = Subst.fromMap . M.fromList <$> arbitrary++instance CoArbitrary Subst' where+    coarbitrary = coarbitrary . M.toList . Subst.toMap
+ test/CriticalPair.hs view
@@ -0,0 +1,57 @@+-- 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++-- Tests for Data.Rewriting.CriticalPair++module CriticalPair where++import Arbitrary+import Samples++import Data.Rewriting.Term (Term (..))+import qualified Data.Rewriting.Term as Term+import Data.Rewriting.Rule (Rule (..))+import Data.Rewriting.Pos (Pos)+import qualified Data.Rewriting.Substitution as Subst+import qualified Data.Rewriting.Rules as Rules+import qualified Data.Rewriting.Context as Ctxt+import Data.Rewriting.CriticalPair++import qualified Data.Set as S+import Test.HUnit++type CP' = CP Fun' Var' Var'++maxSize = 4++propValidCPs' :: [Rule'] -> Bool+propValidCPs' = all validCP . cps' . take maxSize++-- propValidCPs :: [Rule'] -> [Rule'] -> Bool+-- propValidCPs rs rs' = all validCP (cps (take maxSize rs) (take maxSize rs'))++propOuterCPs' :: [Rule'] -> Bool+propOuterCPs' = all (null . leftPos) . cpsOut' . take maxSize++propInnerCPs' :: [Rule'] -> Bool+propInnerCPs' = all (not . null . leftPos) . cpsIn' . take maxSize++tests :: Test+tests = TestLabel "Critical Pair Tests" $ TestList [+    TestCase $ assertEqual "CPs of fixed TRS"+        (cpSet cps1) (cpSet $ cps' trs1)+    ]++cpSet :: (Ord f, Ord v) => [CP f v v] -> S.Set (Term f (Either v v), Term f (Either v v), Term f (Either v v), Rule f v, Rule f v, Pos)+cpSet = S.fromList . map (\cp -> (top cp, left cp, right cp, leftRule cp, rightRule cp, leftPos cp))++validCP :: (Ord v, Eq f) => CP f v v -> Bool+validCP CP{ left = left, top = top, right = right, leftPos = pos,+            leftRule = lRule, rightRule = rRule, subst = subst } =+    subst `Subst.apply` Term.map id Right (lhs rRule) == top &&+    subst `Subst.apply` Term.map id Right (rhs rRule) == right &&+    subst `Subst.apply` Term.map id Left (lhs lRule) == top !!! pos &&+    subst `Subst.apply` Term.map id Left (rhs lRule) == left !!! pos &&+    Ctxt.ofTerm top pos == Ctxt.ofTerm left pos
+ test/Pos.hs view
@@ -0,0 +1,19 @@+-- 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++-- Tests for Data.Rewriting.Pos++module Pos where++import Data.Rewriting.Pos++import Test.QuickCheck++propParallelTo :: Pos -> Pos -> Bool+propParallelTo = \p q -> parallelTo p q == parallelToRef p q++-- reference implementation+parallelToRef :: Pos -> Pos -> Bool+parallelToRef p q = not (p `above` q) && not (p `below` q)
+ test/Rule.hs view
@@ -0,0 +1,47 @@+-- 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++-- Tests for Data.Rewriting.Rules++module Rule where++import Samples+import Arbitrary++import Data.Rewriting.Rule++import Test.HUnit++tests :: Test+tests = TestLabel "Rules Tests" $ TestList [+    TestCase $ assertEqual "isLeftLinear"+        True (isLeftLinear $ x --> f[x, x]),+    TestCase $ assertEqual "~isLeftLinear"+        False (isLeftLinear $ f[x,g[a,b,x],y] --> z),+    TestCase $ assertEqual "isCollapsing"+        True (isCollapsing $ g[a, b] --> x),+    TestCase $ assertEqual "~isCollapsing"+        False (isCollapsing $ z --> g[x,h[x]]),+    TestList []]++propLeftRightLinearDual :: Term' -> Term' -> Bool+propLeftRightLinearDual = dual isLeftLinear isRightLinear++propCollapsingExpandingDual :: Term' -> Term' -> Bool+propCollapsingExpandingDual = dual isCollapsing isExpanding++propErasingCreatingDual :: Term' -> Term' -> Bool+propErasingCreatingDual = dual isErasing isCreating++propLinear :: Term' -> Term' -> Bool+propLinear l r = isLinear (Rule l r) ==+    (isLeftLinear (Rule l r) && isRightLinear (Rule l r))++propValid :: Term' -> Term' -> Bool+propValid l r = isValid (Rule l r) ==+    not (isCreating (Rule l r) || isExpanding (Rule l r))++dual :: (Rule' -> Bool) -> (Rule' -> Bool) -> Term' -> Term' -> Bool+dual p q a b = p (Rule a b) == q (Rule b a)
+ test/Samples.hs view
@@ -0,0 +1,54 @@+-- 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++{-# LANGUAGE StandaloneDeriving #-}++-- selected samples for tests++module Samples where++import Data.Rewriting.Term (Term (..))+import qualified Data.Rewriting.Term as Term+import Data.Rewriting.Rule (Rule (..))+import Data.Rewriting.Pos (Pos)+import Data.Rewriting.CriticalPair (CP (..))+import Data.Rewriting.Substitution (GSubst (..))+import qualified Data.Rewriting.Substitution as Subst+import qualified Data.Rewriting.Context as Ctxt++a = Fun 'a' []+b = Fun 'b' []+c = Fun 'c' []++f = Fun 'f'+g = Fun 'g'+h = Fun 'h'++x = Var 'x'+y = Var 'y'+z = Var 'z'++(-->) = Rule++trs1 = [f[x, x] --> g[a, x], f[a, y] --> h[a], a --> b]+cps1 = [mkCP r1 r2 [], mkCP r3 r2 [0]]+   where [r1, r2, r3] = trs1++mkCP :: (Eq f, Ord v) => Rule f v -> Rule f v -> Pos -> CP f v v+mkCP lRule rRule pos = let+    (llhs, lrhs) = (Term.map id Left (lhs lRule), Term.map id Left (rhs lRule))+    (rlhs, rrhs) = (Term.map id Right (lhs rRule), Term.map id Right (rhs rRule))+    Just subst = Subst.unify llhs (rlhs !!! pos)+    Just rlhs' = Ctxt.ofTerm rlhs pos+  in+    CP{ top = subst `Subst.apply` rlhs, right = subst `Subst.apply` rrhs,+        left = rlhs' `Ctxt.apply` (subst `Subst.apply` lrhs),+        leftRule = lRule, rightRule = rRule, leftPos = pos, subst = subst }++deriving instance (Show f, Show v, Show v') => Show (CP f v v')++(!!!) :: Term f v -> Pos -> Term f v+t !!! [] = t+Fun _ ts !!! (p:ps) = (ts !! p) !!! ps
+ test/Substitution.hs view
@@ -0,0 +1,37 @@+-- 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++-- Tests for Data.Rewriting.Substitution++module Substitution where++import Arbitrary++import Data.Rewriting.Term (Term (..))+import Data.Rewriting.Substitution+import Data.Rewriting.Substitution.Type++import Control.Applicative+import Control.Monad+import Data.Maybe+import Data.Function+import qualified Data.Map as M++propCompose :: Subst' -> Subst' -> Term' -> Bool+propCompose s1 s2 t = (s1 `compose` s2) `apply` t == s1 `apply` (s2 `apply` t)++propUnify1 :: Term' -> Term' -> Bool+propUnify1 s t = Just False /= do+    (\u -> u `apply` s == u `apply` t) <$> unify s t++propUnify2 :: Term' -> Term' -> Bool+propUnify2 s t = Just False /= do+    equalSubst <$> unify s t <*> unifyRef s t++equalSubst :: (Ord v, Eq f) => Subst f v -> Subst f v -> Bool+equalSubst s1 s2 = ((==) `on` toMap) (id' `compose` s1) (id' `compose` s2)+  where+    id' = fromMap . M.fromList $+        [(v, Var v) | v <- M.keys (toMap s1) ++ M.keys (toMap s2)]
+ test/Term.hs view
@@ -0,0 +1,28 @@+-- 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++-- Tests for Data.Rewriting.Term++module Term where++import Arbitrary++import Data.Rewriting.Pos+import Data.Rewriting.Term++import Control.Monad (liftM2)+import Data.Maybe (fromMaybe)++propReplaceAt1 :: Pos -> Term' -> Term' -> Bool+propReplaceAt1 p t t' = fromMaybe True $ do+    u <- replaceAt t p t'+    v <- u `subtermAt` p+    return $ t' == v++propReplaceAt2 :: Pos -> Term' -> Term' -> Term' -> Bool+propReplaceAt2 p t t1 t2 = fromMaybe True $ do+    u1 <- replaceAt t p t1+    u2 <- replaceAt t p t2+    return $ (u1 == u2) == (t1 == t2)