term-rewriting 0.2 → 0.2.1

raw patch · 7 files changed

+52/−14 lines, 7 filesdep ~basedep ~multiset

Dependency ranges changed: base, multiset

Files

• LICENSE +1/−1
• src/Data/Rewriting/Problem/Type.hs +26/−1
• src/Data/Rewriting/Rule/Ops.hs +3/−3
• src/Data/Rewriting/Rule/Type.hs +10/−2
• src/Data/Rewriting/Rules/Ops.hs +10/−2
• src/Data/Rewriting/Substitution/Pretty.hs +0/−3
• term-rewriting.cabal +2/−2

@@ -1,6 +1,6 @@ term-rewriting library -- basic first order term rewriting. -Copyright (c) 2011-2013 by Martin Avanzini, Bertram Felgenhauer and+Copyright (c) 2011-2017 by Martin Avanzini, Bertram Felgenhauer and Christian Sternagel.  Permission is hereby granted, free of charge, to any person obtaining a

@@ -9,10 +9,15 @@   RulesPair (..),   Problem (..),   Theory (..),-  allRules+  allRules,+  map  ) where +import Prelude hiding (map)+import qualified Prelude as P+ import Data.Rewriting.Rule (Rule (..))+import qualified Data.Rewriting.Rule as Rule  data StartTerms = AllTerms                 | BasicTerms deriving (Eq, Show)@@ -38,3 +43,23 @@  allRules :: RulesPair f v -> [Rule f v] allRules rp = strictRules rp ++ weakRules rp++map :: (f -> f') -> (v -> v') -> Problem f v -> Problem f' v'+map ffun fvar prob = +   Problem { startTerms = startTerms prob +           , strategy = strategy prob+           , theory = P.map (mapTheory ffun fvar) <$> theory prob +           , rules = mapRulesPair ffun fvar (rules prob)+           , variables = P.map fvar (variables prob)+           , symbols = P.map ffun (symbols prob)+           , comment = comment prob}+              +mapTheory :: (f -> f') -> (v -> v') -> Theory f v -> Theory f' v'+mapTheory ffun _ (SymbolProperty p fs) = SymbolProperty p (P.map ffun fs)+mapTheory ffun fvar (Equations rs) = Equations (P.map (Rule.map ffun fvar) rs)++mapRulesPair :: (f -> f') -> (v -> v') -> RulesPair f v -> RulesPair f' v'+mapRulesPair ffun fvar rp = +    RulesPair { strictRules = modify (strictRules rp)+              , weakRules = modify (weakRules rp)}+        where modify = P.map (Rule.map ffun fvar)

@@ -47,10 +47,10 @@ right f = f . rhs  --- | Lifting of 'Term.rename' to 'Rule': renames left- and--- right-hand sides.+-- | 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]}+-- 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) 

@@ -6,14 +6,22 @@ module Data.Rewriting.Rule.Type (     module Data.Rewriting.Term.Type,     Rule (..),+    map,+    mapSides ) where +import Prelude hiding (map) import Data.Rewriting.Term.Type hiding (map, fold)+import qualified Data.Rewriting.Term.Type as T  -- | Rewrite rule with left-hand side and right-hand side. data Rule f v = Rule { lhs :: Term f v, rhs :: Term f v }     deriving (Ord, Eq, Show) --- mapRule :: (Term f v -> Term f' v') -> Rule f v -> Rule f' v'--- mapRule f r = Rule{ lhs = f (lhs r), rhs = f (rhs r) }++mapSides :: (Term f v -> Term f' v') -> Rule f v -> Rule f' v'+mapSides f r = Rule{ lhs = f (lhs r), rhs = f (rhs r) }++map :: (f -> f') -> (v -> v') -> Rule f v -> Rule f' v'+map f v = mapSides (T.map f v) 

@@ -11,17 +11,21 @@     varsDL,     lhss,     rhss,+    map,     restrictFuns,     -- * Predicates on Rules     isLinear, isLeftLinear, isRightLinear,     isGround, isLeftGround, isRightGround,     isErasing,     isCreating,+    isExpanding,     isDuplicating,     isCollapsing,     isValid, ) where +import Prelude hiding (map)+import qualified Prelude as P import Data.Rewriting.Rule (Rule) import Data.Rewriting.Term (Term) import qualified Data.Rewriting.Term as Term@@ -30,11 +34,11 @@  -- | @lhss rs@ returns the list of left-hand sides of @rs@ lhss :: [Rule f v] -> [Term f v]-lhss = map Rule.lhs+lhss = P.map Rule.lhs  -- | @lhss rs@ returns the list of right-hand sides of @rs@ rhss :: [Rule f v] -> [Term f v]-rhss = map Rule.rhs+rhss = P.map Rule.rhs  -- | Lifting of Term.'Term.funs' to list of rules. funs :: [Rule f v] -> [f]@@ -48,6 +52,10 @@ -- | Lifting of Term.'Term.vars' to list of rules. vars :: [Rule f v] -> [v] vars = flip varsDL []++-- | Lifting of Rule.'Rule.map' to list of rules.+map :: (f -> f') -> (v -> v') -> [Rule f v] -> [Rule f' v']+map f v = P.map (Rule.map f v)  -- | Difference List version of 'vars'. -- We have @varsDL r vs = vars r ++ vs@.

@@ -24,6 +24,3 @@  instance (Pretty v, Pretty f, Pretty v') => Pretty (GSubst v f v') where     pretty = prettyGSubst pretty pretty pretty--instance (Pretty f, Pretty v) => Pretty (Subst f v) where-    pretty = prettySubst pretty pretty

@@ -1,5 +1,5 @@ name:          term-rewriting-version:       0.2+version:       0.2.1 stability:     experimental author:        Martin Avanzini,                Bertram Felgenhauer,@@ -65,7 +65,7 @@         Data.Rewriting.Utils.Parse     build-depends:         containers >= 0.3 && < 0.6,-        multiset >= 0.2 && < 0.3,+        multiset >= 0.2 && < 0.4,         parsec >= 3.1.6 && < 3.2,         union-find-array >= 0.1 && < 0.2,         array >= 0.3 && < 0.6,