packages feed

term-rewriting (empty) → 0.1

raw patch · 35 files changed

+1862/−0 lines, 35 filesdep +ansi-wl-pprintdep +arraydep +basesetup-changed

Dependencies added: ansi-wl-pprint, array, base, containers, mtl, multiset, parsec, union-find-array

Files

+ LICENSE view
@@ -0,0 +1,22 @@+term-rewriting library -- basic first order term rewriting.++Copyright (c) 2011-2013 by Martin Avanzini, Bertram Felgenhauer and+Christian Sternagel.++Permission is hereby granted, free of charge, to any person obtaining a+copy of this software and associated documentation files (the "Software"),+to deal in the Software without restriction, including without limitation+the rights to use, copy, modify, merge, publish, distribute, sublicense,+and/or sell copies of the Software, and to permit persons to whom the+Software is furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER+DEALINGS IN THE SOFTWARE.
+ Setup.lhs view
@@ -0,0 +1,3 @@+#! /usr/bin/env runghc+> import Distribution.Simple (defaultMain)+> main = defaultMain
+ src/Data/Rewriting/Context.hs view
@@ -0,0 +1,17 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Author: Bertram Felgenhauer++module Data.Rewriting.Context (+    Ctxt,+    -- * Important operations+    ofTerm,+    apply,+    -- * Reexported modules+    module Data.Rewriting.Context.Type,+    module Data.Rewriting.Context.Ops,+) where++import Data.Rewriting.Context.Type+import Data.Rewriting.Context.Ops
+ src/Data/Rewriting/Context/Ops.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: Christian Sternagel++module Data.Rewriting.Context.Ops (+    apply,+    compose,+    ofTerm,+) where++import Control.Monad+import Data.Rewriting.Pos+import Data.Rewriting.Term.Type+import Data.Rewriting.Context.Type++-- | Apply a context to a term (i.e., replace the hole in the context by the+-- term).+apply :: Ctxt f v -> Term f v -> Term f v+apply Hole t = t+apply (Ctxt f ts1 ctxt ts2) t = Fun f (ts1 ++ apply ctxt t : ts2)++-- | Compose two contexts (i.e., replace the hole in the left context by the+-- right context).+compose :: Ctxt f v -> Ctxt f v -> Ctxt f v+compose Hole c2 = c2+compose (Ctxt f ts1 c1 ts2) c2 = Ctxt f ts1 (c1 `compose` c2) ts2++-- | Create a context from a term by placing the hole at a specific position.+ofTerm :: Term f v -> Pos -> Maybe (Ctxt f v)+ofTerm _ [] = Just Hole+ofTerm (Fun f ts) (i:p) = do+    guard (i >= 0 && i < length ts)+    let (ts1, t:ts2) = splitAt i ts+    ctxt <- ofTerm t p+    return (Ctxt f ts1 ctxt ts2)+ofTerm _ _ = Nothing
+ src/Data/Rewriting/Context/Type.hs view
@@ -0,0 +1,17 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Christian Sternagel++module Data.Rewriting.Context.Type (+    Ctxt (..),+) where++import Data.Rewriting.Term (Term(..))++data Ctxt f v+    = Hole                                    -- ^ Hole+    | Ctxt f [Term f v] (Ctxt f v) [Term f v] -- ^ Non-empty context++    -- CS: would it make sense to reverse the left term list?+    deriving (Show, Eq, Ord)
+ src/Data/Rewriting/CriticalPair.hs view
@@ -0,0 +1,17 @@+-- 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++module Data.Rewriting.CriticalPair (+    CP,+    -- * Important operations+    cps',+    cps,+    -- * Reexported modules+    module Data.Rewriting.CriticalPair.Type,+    module Data.Rewriting.CriticalPair.Ops,+) where++import Data.Rewriting.CriticalPair.Type+import Data.Rewriting.CriticalPair.Ops
+ src/Data/Rewriting/CriticalPair/Ops.hs view
@@ -0,0 +1,140 @@+-- 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++module Data.Rewriting.CriticalPair.Ops (+    -- * pairs of rewrite systems+    cps,+    cpsIn,+    cpsOut,+    -- * single rewrite systems+    cps',+    cpsIn',+    cpsOut',+) where++import Data.Rewriting.CriticalPair.Type+import Data.Rewriting.Substitution+import Data.Rewriting.Rule.Type+import qualified Data.Rewriting.Term as Term+import Data.Rewriting.Pos+import Data.Rewriting.Rules.Rewrite (listContexts)++import Data.Maybe+import Control.Monad+import Data.List++-- cpW does all the hard work:+-- Given a function that returns contexts to consider for rewriting,+-- unify the contexts of the right rule's lhs with the left rule's lhs,+-- and return the resulting critical pairs.+cpW :: (Ord v, Ord v', Eq f)+    => (Term f (Either v v')+        -> [(Pos, Context f (Either v v'), Term f (Either v v'))])+    -> Rule f v -> Rule f v' -> [(CP f v v')]+cpW f rl rr = do+    let rl' = Term.map id Left (lhs rl)+        rr' = Term.map id Right (lhs rr)+    (pos, ctx, rr'') <- f rr'+    guard $ not (Term.isVar rr'')+    subst <- maybeToList $ unify rl' rr''+    return CP{+        left = apply subst (ctx (Term.map id Left (rhs rl))),+        top = apply subst rr',+        right = apply subst (Term.map id Right (rhs rr)),+        leftRule = rl,+        leftPos = pos,+        rightRule = rr,+        subst = subst+    }+++-- TODO: find a better place for this kind of contexts.+type Context f v = Term f v -> Term f v++-- Calculate contexts of a term, in pre-order.+-- In particular, the root context is returned first.+contexts :: Term f v -> [(Pos, Context f v, Term f v)]+contexts t@(Var _)    = [([], id, t)]+contexts t@(Fun f ts) = ([], id, t) : do+    (i, ctxL, t) <- listContexts ts+    (pos, ctxT, t') <- contexts t+    return (i : pos, Fun f . ctxL . ctxT, t')++-- Determine critical pairs for a pair of rules.+cp :: (Ord v, Ord v', Eq f)+    => Rule f v -> Rule f v' -> [(CP f v v')]+cp  = cpW contexts++-- Determine outer critical pairs for a pair of rules.+cpOut :: (Ord v, Ord v', Eq f)+    => Rule f v -> Rule f v' -> [(CP f v v')]+cpOut = cpW (take 1 . contexts)++-- Determine inner critical pairs for a pair of rules.+cpIn :: (Ord v, Ord v', Eq f)+    => Rule f v -> Rule f v' -> [(CP f v v')]+cpIn = cpW (tail . contexts)+++-- | Determine all critical pairs for a pair of TRSs.+cps :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v']+    -> [(CP f v v')]+cps  trs1 trs2 = do+    rl <- trs1+    rr <- trs2+    cp rl rr++-- | Determine all inner critical pairs for a pair of TRSs.+--+-- A critical pair is /inner/ if the left rewrite step is not a root step.+cpsIn :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v']+    -> [(CP f v v')]+cpsIn trs1 trs2 = do+    rl <- trs1+    rr <- trs2+    cpOut rl rr++-- | Determine outer critical pairs for a pair of TRSs.+--+-- A critical pair is /outer/ if the left rewrite step is a root step.+cpsOut :: (Ord v, Ord v', Eq f) => [Rule f v] -> [Rule f v']+    -> [(CP f v v')]+cpsOut trs1 trs2 = do+    rl <- trs1+    rr <- trs2+    cpIn rl rr+++-- | Determine all critical pairs of a single TRS with itself.+--+-- Unlike @cps@, @cps'@ takes symmetries into account. See 'cpsIn'' and+-- 'cpsOut'' for details.+cps' :: (Ord v, Eq f) => [Rule f v] -> [(CP f v v)]+cps'  trs = cpsIn' trs ++ cpsOut' trs++-- | Determine all inner critical pairs of a single TRS with itself.+--+-- The result of @cpsIn' trs@ differs from @cpsIn trs trs@ in that overlaps+-- of a rule with itself are returned once, not twice.+cpsIn' :: (Ord v, Eq f) => [Rule f v] -> [(CP f v v)]+cpsIn' trs = do+    r1 : trs' <- tails trs+    cpIn r1 r1 ++ do+        r2 <- trs'+        cpIn r1 r2 ++ cpIn r2 r1++-- | Determine all outer critical pairs of a single TRS with itself.+--+-- The result of @cpsOut' trs@ differs from @cpsOut trs trs@ in two aspects:+--+--  * The trivial overlaps of rules with themselves are omitted.+--+--  * Symmetry is taken into account: Overlaps between distinct rules are+--    returned once instead of twice.+cpsOut' :: (Ord v, Eq f) => [Rule f v] -> [(CP f v v)]+cpsOut' trs = do+    rl : trs' <- tails trs+    rr <- trs'+    cpOut rl rr
+ src/Data/Rewriting/CriticalPair/Type.hs view
@@ -0,0 +1,33 @@+-- 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++module Data.Rewriting.CriticalPair.Type (+    CP (..),+) where++import Data.Rewriting.Substitution+import Data.Rewriting.Rule.Type+import Data.Rewriting.Pos++-- | A critical pair. Critical pairs (should) have the following properties:+--+-- @+-- top   == Context.ofTerm top pos (Term.map Left id (Rule.lhs leftRule))+-- left  == Context.ofTerm top pos (Term.map Left id (Rule.rhs leftRule))+-- top   == Substitution.apply subst (Term.map Right id (Rule.lhs rightRule))+-- right == Substitution.apply subst (Term.map Right id (Rule.rhs rightRule))+-- @+--+-- Furthermore, @pos@ is a non-variable position of @(lhs rightRule)@ and+-- @subst@ is a most general substitution with these properties.+data CP f v v' = CP {+    left :: Term f (Either v v'),  -- ^ left reduct+    top :: Term f (Either v v'),   -- ^ source+    right :: Term f (Either v v'), -- ^ right reduct+    leftRule :: Rule f v,          -- ^ rule applied on left side+    leftPos :: Pos,                -- ^ position of left rule application+    rightRule :: Rule f v',        -- ^ rule applied on right side+    subst :: Subst f (Either v v') -- ^ common substitution of the rewrite steps+}
+ src/Data/Rewriting/Pos.hs view
@@ -0,0 +1,59 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Christian Sternagel, Bertram Felgenhauer, Martin Avanzini++module Data.Rewriting.Pos (+    Pos,+    -- * Comparing Positions+    -- | Note that positions are not totally ordered. Nevertheless there are+    -- some commonly useful comparisons between positions.+    above,+    below,+    parallelTo,+    leftOf,+    rightOf,+) where++import Data.Rewriting.Utils+import Data.List++-- | A position in a term. Arguments are counted from 0.+--+-- A position describes a path in the tree representation of a term. The empty+-- position @[]@ denotes the root of the term. A position @[0,1]@ denotes the+-- 2nd child of the 1st child of the root (counting children from left to+-- right).+type Pos = [Int]++-- | @p \`above\` q@ checks whether @p@ is above @q@ (in the tree representation of+-- a term). A position @p@ is above a position @q@, whenever @p@ is a prefix of+-- @q@.+above :: Pos -> Pos -> Bool+above = isPrefixOf++-- | @p \`below\` q@ checks whether @p@ is below @q@, that is to say that @q@ is+-- above @p@.+below :: Pos -> Pos -> Bool+below = flip above++-- | @p \`parallelTo\` q@ checks whether @p@ is parallel to @q@, that is to say+-- that @p@ and @q@ do not lie on the same path.+parallelTo :: Pos -> Pos -> Bool+parallelTo p q = not (null p') && not (null q') where+    (p', q') = dropCommonPrefix p q++-- | @p \`leftOf\` q@ checks whether @p@ is left of @q@. This is only possible if+-- @p@ and @q@ do not lie on the same path (i.e., are parallel to each other).+leftOf :: Pos -> Pos -> Bool+leftOf p q = not (null p') && not (null q') && head p' < head q' where+    (p', q') = dropCommonPrefix p q++-- | @p \`rightOf\` q@ checks whether @p@ is right of @q@.+rightOf :: Pos -> Pos -> Bool+rightOf p q = not (null p') && not (null q') && head p' > head q' where+    (p', q') = dropCommonPrefix p q++-- reference implementations+parallelToRef :: Pos -> Pos -> Bool+parallelToRef p q = not (p `above` q) && not (p `below` q)
+ src/Data/Rewriting/Problem.hs view
@@ -0,0 +1,17 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini++-- | Termination problem type, based on WST format.+module Data.Rewriting.Problem (+    Problem,+    -- * Reexported modules+    module Data.Rewriting.Problem.Type,+    module Data.Rewriting.Problem.Parse,+    module Data.Rewriting.Problem.Pretty,+) where++import Data.Rewriting.Problem.Type+import Data.Rewriting.Problem.Parse+import Data.Rewriting.Problem.Pretty
+ src/Data/Rewriting/Problem/Parse.hs view
@@ -0,0 +1,150 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini, Christian Sternagel++{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Data.Rewriting.Problem.Parse (+  parseIO,+  parseFileIO,+  fromString,+  fromFile,+  fromCharStream,+  ProblemParseError (..)+  ) where++import Data.Rewriting.Utils.Parse (lex, par, ident)+import qualified Data.Rewriting.Problem.Type as Prob+import Data.Rewriting.Problem.Type (Problem)+import Data.Rewriting.Rule (Rule (..))+import qualified Data.Rewriting.Term as Term+import qualified Data.Rewriting.Rules as Rules++import Data.List (partition, union)+import Data.Maybe (isJust)+import Prelude hiding (lex, catch)+import Control.Exception (catch)+import Control.Monad.Error+import Control.Monad (liftM, liftM3)+import Text.Parsec hiding (parse)+import System.IO (readFile)++data ProblemParseError = UnknownParseError String+                       | UnsupportedStrategy String+                       | FileReadError IOError+                       | UnsupportedDeclaration String+                       | SomeParseError ParseError deriving (Show)++instance Error ProblemParseError where strMsg = UnknownParseError++parseFileIO :: FilePath -> IO (Problem String String)+parseFileIO file = do r <- fromFile file+                      case r of+                        Left err -> do { putStrLn "following error occured:"; print err; mzero }+                        Right t  -> return t++parseIO :: String -> IO (Problem String String)+parseIO string = case fromString string of+                    Left err -> do { putStrLn "following error occured:"; print err; mzero }+                    Right t  -> return t++fromFile :: FilePath -> IO (Either ProblemParseError (Problem String String))+fromFile file = fromFile' `catch` (return . Left . FileReadError) where+  fromFile' = fromCharStream sn `liftM` readFile file+  sn         = "<file " ++ file ++ ">"++fromString :: String -> Either ProblemParseError (Problem String String)+fromString = fromCharStream "supplied string"++fromCharStream :: (Stream s (Either ProblemParseError) Char)+                   => SourceName -> s -> Either ProblemParseError (Problem String String)+fromCharStream sourcename input =+  case runParserT parse initialState sourcename input of+    Right (Left e)  -> Left $ SomeParseError e+    Right (Right p) -> Right p+    Left e          -> Left e+  where initialState = Prob.Problem { Prob.startTerms = Prob.AllTerms ,+                                      Prob.strategy   = Prob.Full ,+                                      Prob.theory     = Nothing ,+                                      Prob.rules      = Prob.RulesPair { Prob.strictRules = [],+                                                                         Prob.weakRules = [] } ,+                                      Prob.variables  = [] ,+                                      Prob.symbols    = [] ,+                                      Prob.comment    = Nothing }+++type ParserState = Problem String String++type WSTParser s a = ParsecT s ParserState (Either ProblemParseError) a++modifyProblem :: (Problem String String -> Problem String String) -> WSTParser s ()+modifyProblem = modifyState++parsedVariables :: WSTParser s [String]+parsedVariables = Prob.variables `liftM` getState++parse :: (Stream s (Either ProblemParseError) Char) => WSTParser s (Problem String String)+parse = spaces >> parseDecls >> eof >> getState where+  parseDecls = many1 parseDecl+  parseDecl =  decl "VAR"       vars       (\ e p -> p {Prob.variables = e `union` Prob.variables p})+           <|> decl "THEORY"    theory     (\ e p -> p {Prob.theory = maybeAppend Prob.theory e p})+           <|> decl "RULES"     rules      (\ e p -> p {Prob.rules   = e, --FIXME multiple RULES blocks?+                                                        Prob.symbols = Rules.funsDL (Prob.allRules e) [] })+           <|> decl "STRATEGY"  strategy   (\ e p -> p {Prob.strategy = e})+           <|> decl "STARTTERM" startterms (\ e p -> p {Prob.startTerms = e})+           <|> (par comment >>= modifyProblem . (\ e p -> p {Prob.comment = maybeAppend Prob.comment e p}) <?> "comment")+  decl name p f = try (par $ do+      lex $ string name+      r <- p+      modifyProblem $ f r) <?> (name ++ " block")+  maybeAppend fld e p = Just $ maybe [] id (fld p) ++ e++vars :: (Stream s (Either ProblemParseError) Char) => WSTParser s [String]+vars = do vs <- many (lex $ ident "()," [])+          return vs++theory :: (Stream s (Either ProblemParseError) Char) => WSTParser s [Prob.Theory String String]+theory = many thdecl where+    thdecl     = par ((equations >>= return . Prob.Equations)+              <|>     (idlist    >>= \ (x:xs) -> return $ Prob.SymbolProperty x xs))+    equations  = try (do+        vs <- parsedVariables+        lex $ string "EQUATIONS"+        many $ equation vs) <?> "EQUATIONS block"+    equation vs = do+        l <- Term.parseWST vs+        lex $ string "=="+        r <- Term.parseWST vs+        return $ Rule l r+    idlist      = many1 $ (lex $ ident "()," [])++rules :: (Stream s (Either ProblemParseError) Char) => WSTParser s (Prob.RulesPair String String)+rules = do vs <- parsedVariables+           rs <- many $ rule vs+           let (s,w) = partition fst rs+           return Prob.RulesPair { Prob.strictRules = map snd s ,+                                   Prob.weakRules   = map snd w }+  where rule vs = do l <- Term.parseWST vs+                     sep <- lex $ (try $ string "->=") <|> string "->"+                     r <- Term.parseWST vs+                     return (sep == "->", Rule {lhs = l, rhs = r})++strategy :: (Stream s (Either ProblemParseError) Char) => WSTParser s Prob.Strategy+strategy = innermost <|> outermost where+  innermost = string "INNERMOST" >> return Prob.Innermost+  outermost = string "OUTERMOST" >> return Prob.Outermost++startterms :: (Stream s (Either ProblemParseError) Char) => WSTParser s Prob.StartTerms+startterms = basic <|> terms where+  basic = string "CONSTRUCTOR-BASED" >> return Prob.BasicTerms+  terms = string "FULL" >> return Prob.AllTerms++comment :: (Stream s (Either ProblemParseError) Char) => WSTParser s String+comment = withpars <|> liftM2 (++) idents comment <|> return ""+  where idents = many1 (noneOf "()")+        withpars = do _ <- char '('+                      pre <- comment+                      _ <- char ')'+                      suf <- comment+                      return $ "(" ++ pre ++ ")" ++ suf
+ src/Data/Rewriting/Problem/Pretty.hs view
@@ -0,0 +1,89 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini++module Data.Rewriting.Problem.Pretty (+    prettyProblem,+    prettyWST,+    prettyWST',+) where++import Data.Maybe (isJust, fromJust)+import Data.List (nub)+import Data.Rewriting.Problem.Type+import Data.Rewriting.Rule (prettyRule)+import Text.PrettyPrint.ANSI.Leijen++printWhen :: Bool -> Doc -> Doc+printWhen False _ = empty+printWhen True  p = p+++prettyWST' :: (Pretty f, Pretty v) => Problem f v -> Doc+prettyWST' = prettyWST pretty pretty++prettyWST :: (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc+prettyWST fun var prob =+    printWhen (sterms /= AllTerms) (block "STARTTERM" $ text "CONSTRUCTOR-BASED")+    <$$> printWhen (strat /= Full) (block "STRATEGY" $ ppStrat strat)+    <$$> maybeblock "THEORY" theory ppTheories+    <$$> block "VAR" (ppVars $ variables prob)+    <$$> block "RULES" (ppRules $ rules prob)+    <$$> maybeblock "COMMENT" comment text++  where block n pp = parens $ hang 3 $ text n <$$> pp+        maybeblock n f fpp = case f prob of+                               Just e -> block n (fpp e)+                               Nothing -> empty++        ppStrat Innermost = text "INNERMOST"+        ppStrat Outermost = text "OUTERMOST"++        ppVars vs = align $ fillSep [ var v | v <- vs]++        ppTheories thys = align $ vcat [ppThy thy | thy <- thys]+            where ppThy (SymbolProperty p fs) = block p (align $ fillSep [ fun f | f <- fs ])+                  ppThy (Equations rs)        = block "EQUATIONS" $ vcat [ppRule "==" r | r <- rs]++        ppRules rp = align $ vcat ([ppRule "->" r | r <- strictRules rp]+                                   ++ [ppRule "->=" r | r <- weakRules rp])++        ppRule sep = prettyRule (text sep) fun var++        sterms = startTerms prob+        strat  = strategy prob+        thry   = theory prob+++prettyProblem :: (Eq f, Eq v) => (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc+prettyProblem fun var prob =  block "Start-Terms" (ppST `on` startTerms)+                              <$$> block "Strategy" (ppStrat `on` strategy)+                              <$$> block "Variables" (ppVars `on` variables)+                              <$$> block "Function Symbols" (ppSyms `on` symbols)+                              <$$> maybeblock "Theory" ppTheories theory+                              <$$> block "Rules" (ppRules `on` rules)+                              <$$> maybeblock "Comment" ppComment comment where+  pp `on` fld = pp $ fld prob+  block n pp = hang 3 $ (underline $ text $ n ++ ":") <+> pp+  maybeblock n pp f = printWhen (isJust `on` f) (block n (pp `on` (fromJust . f)))+  commalist  = fillSep . punctuate (text ",")++  ppST AllTerms      = text "all"+  ppST BasicTerms    = text "basic terms"+  ppStrat Innermost  = text "innermost"+  ppStrat Outermost  = text "outermost"+  ppStrat Full       = text "full rewriting"+  ppVars vars        = commalist $ [var v | v <- nub vars]+  ppSyms syms        = commalist $ [fun v | v <- nub syms]+  ppComment c        = text c+  ppTheories ths     =  align $ vcat [ ppTheory th | th <- ths ] where+      ppTheory (SymbolProperty p fs) = text (p++":") <+> align (commalist [ fun f | f <- fs])+      ppTheory (Equations rs)        = align $ vcat [ppRule "==" r | r <- rs]+  ppRules rp         = align $ vcat $+                       [ppRule "->" r | r <- strictRules rp]+                       ++ [ppRule "->=" r | r <- weakRules rp]+  ppRule sep         = prettyRule (text sep) fun var++instance (Eq f, Eq v, Pretty f, Pretty v) => Pretty (Problem f v) where+  pretty = prettyProblem pretty pretty
+ src/Data/Rewriting/Problem/Type.hs view
@@ -0,0 +1,40 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini, Christial Sternagel++module Data.Rewriting.Problem.Type (+  StartTerms (..),+  Strategy (..),+  RulesPair (..),+  Problem (..),+  Theory (..),+  allRules+ ) where++import Data.Rewriting.Rule (Rule (..))++data StartTerms = AllTerms+                | BasicTerms deriving (Eq, Show)++data Strategy = Innermost+              | Full+              | Outermost deriving (Eq, Show)++data RulesPair f v = RulesPair { strictRules :: [Rule f v]+                               , weakRules   :: [Rule f v] } deriving (Eq, Show)+++data Theory f v = SymbolProperty String [f]+                | Equations [Rule f v] deriving (Eq, Show)++data Problem f v = Problem { startTerms :: StartTerms+                           , strategy   :: Strategy+                           , theory     :: Maybe [Theory f v]+                           , rules      :: RulesPair f v+                           , variables  :: [v]+                           , symbols    :: [f]+                           , comment    :: Maybe String} deriving (Show)++allRules :: RulesPair f v -> [Rule f v]+allRules rp = strictRules rp ++ weakRules rp
+ src/Data/Rewriting/Rule.hs view
@@ -0,0 +1,16 @@+-- 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, Martin Avanzini++module Data.Rewriting.Rule (+    Rule (..),+    -- * Reexported modules+    module Data.Rewriting.Rule.Type,+    module Data.Rewriting.Rule.Ops,+    module Data.Rewriting.Rule.Pretty,+) where++import Data.Rewriting.Rule.Type+import Data.Rewriting.Rule.Ops+import Data.Rewriting.Rule.Pretty
+ src/Data/Rewriting/Rule/Ops.hs view
@@ -0,0 +1,150 @@+-- 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, Martin Avanzini++module Data.Rewriting.Rule.Ops (+    -- * Operations on Rules+    funs,+    funsDL,+    vars,+    varsDL,+    left,+    right,+    -- * Predicates on Rules+    both,+    isLinear, isLeftLinear, isRightLinear,+    isGround, isLeftGround, isRightGround,+    isErasing,+    isCreating,+    isDuplicating,+    isCollapsing,+    isExpanding,+    isValid,+    isInstanceOf,+    isVariantOf,+) where++import Data.Rewriting.Rule.Type+import Data.Rewriting.Substitution (match, merge)+import qualified Data.Rewriting.Term as Term++import qualified Data.Set as S+import qualified Data.MultiSet as MS+import Data.Maybe++-- | Test whether the given predicate is true for both sides of a rule.+both :: (Term f v -> Bool) -> Rule f v -> Bool+both p r = p (lhs r) && p (rhs r)++-- | Apply a function to the lhs of a rule.+left :: (Term f v -> a) -> Rule f v -> a+left f = f . lhs++-- | 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.funs' to 'Rule': returns the list of function symbols+-- in left- and right-hand sides.+--+-- >>> funs $ Rule {lhs = Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]], rhs = Fun 'h' [Fun 'f' []]}+-- "fgfhf"+funs :: Rule f v -> [f]+funs = flip funsDL []++-- | Difference List version of 'funs'.+-- We have @funsDL r vs = funs r ++ vs@.+funsDL ::  Rule f v -> [f] -> [f]+funsDL r = Term.funsDL (lhs r) . Term.funsDL (rhs r)++-- | Lifting of 'Term.vars' to 'Rule': returns the list of variables in+-- left- and right-hand sides.+--+-- >>> vars $ Rule {lhs = Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]], rhs = Fun 'g' [Var 4, Var 3]}+-- [3,1,2,3,4,3]+vars :: Rule f v -> [v]+vars = flip varsDL []++-- | Difference List version of 'vars'.+-- We have @varsDL r vs = vars r ++ vs@.+varsDL :: Rule f v -> [v] -> [v]+varsDL r = Term.varsDL (lhs r) . Term.varsDL (rhs r)++-- | Check whether both sides of the given rule are linear.+isLinear :: Ord v => Rule f v -> Bool+isLinear = both Term.isLinear++-- | Check whether the left hand side of the given rule is linear.+isLeftLinear :: Ord v => Rule f v -> Bool+isLeftLinear = left Term.isLinear++-- | Check whether the right hand side of the given rule is linear.+isRightLinear :: Ord v => Rule f v -> Bool+isRightLinear = right Term.isLinear++-- | Check whether both sides of the given rule is are ground terms.+isGround :: Rule f v -> Bool+isGround = both Term.isGround++-- | Check whether the left hand side of the given rule is a ground term.+isLeftGround :: Rule f v -> Bool+isLeftGround = left Term.isGround++-- | Check whether the right hand side of the given rule is a ground term.+isRightGround :: Rule f v -> Bool+isRightGround = right Term.isGround++-- auxiliary: return variables of term as Set+varsS :: Ord v => Term f v -> S.Set v+varsS = S.fromList . Term.vars++-- | Check whether the given rule is erasing, i.e., if some variable+-- occurs in the left hand side but not in the right hand side.+isErasing :: Ord v => Rule f v -> Bool+isErasing r = not $ varsS (lhs r) `S.isSubsetOf` varsS (rhs r)++-- | Check whether the given rule is creating, i.e., if some variable+-- occurs in its right hand side that does not occur in its left hand side.+--+-- This is the dual of 'isErasing'. The term /creating/ is non-standard.+-- Creating rules are usually forbidden. See also 'isValid'.+isCreating :: Ord v => Rule f v -> Bool+isCreating r = not $ varsS (rhs r) `S.isSubsetOf` varsS (lhs r)++-- auxiliary: return variables of term as MultiSet+varsMS :: Ord v => Term f v -> MS.MultiSet v+varsMS = MS.fromList . Term.vars++-- | Check whether the given rule is duplicating, i.e., if some variable+-- occurs more often in its right hand side than in its left hand side.+isDuplicating :: Ord v => Rule f v -> Bool+isDuplicating r = not $ varsMS (rhs r) `MS.isSubsetOf` varsMS (lhs r)++-- | Check whether the given rule is collapsing, i.e., if its right+-- hand side is a variable.+isCollapsing :: Rule f v -> Bool+isCollapsing = Term.isVar . rhs++-- | Check whether the given rule is expanding, i.e., if its left hand+-- sides is a variable.+--+-- This is the dual of 'isCollapsing'. The term /expanding/ is non-standard.+-- Expanding rules are usually forbidden. See also 'isValid'.+isExpanding :: Rule f v -> Bool+isExpanding = Term.isVar . lhs++-- | Check whether rule is non-creating and non-expanding.+-- See also 'isCreating' and 'isExpanding'+isValid :: Ord v => Rule f v -> Bool+isValid r = not (isCreating r) && not (isExpanding r)++-- | Check whether a rule is an instance of another.+isInstanceOf :: (Eq f, Ord v, Ord v') => Rule f v -> Rule f v' -> Bool+isInstanceOf r r' = case (match (lhs r) (lhs r'), match (rhs r) (rhs r')) of+    (Just s, Just s') -> isJust (merge s s')+    _ -> False++-- | Check whether a rule is a variant of another.+isVariantOf :: (Eq f, Ord v, Ord v') => Rule f v -> Rule f v' -> Bool+isVariantOf t u = isInstanceOf t u && isInstanceOf u t
+ src/Data/Rewriting/Rule/Pretty.hs view
@@ -0,0 +1,21 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini++module Data.Rewriting.Rule.Pretty (+    prettyRule+)  where++import Data.Rewriting.Rule.Type+import Data.Rewriting.Term (prettyTerm)++import Text.PrettyPrint.ANSI.Leijen++prettyRule :: Doc -> (f -> Doc) -> (v -> Doc) -> Rule f v -> Doc+prettyRule arr fun var (Rule l r) = hang 2 $ term l <+> arr </> term r where+    term = prettyTerm fun var++instance (Pretty f, Pretty v) => Pretty (Rule f v) where+    pretty = prettyRule (text "->") pretty pretty+
+ src/Data/Rewriting/Rule/Type.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++module Data.Rewriting.Rule.Type (+    module Data.Rewriting.Term.Type,+    Rule (..),+) where++import Data.Rewriting.Term.Type hiding (map, fold)++-- | 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) }+
+ src/Data/Rewriting/Rules.hs view
@@ -0,0 +1,22 @@+-- 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, Martin Avanzini++-- | Operations on lists of rules.+--+-- See also "Data.Rewriting.CriticalPair"+module Data.Rewriting.Rules (+    -- * Important operations+    fullRewrite,+    -- * Reexported modules+    module Data.Rewriting.Rules.Rewrite,+    module Data.Rewriting.Rules.Ops,+) where++import Data.Rewriting.Rules.Ops+import Data.Rewriting.Rules.Rewrite hiding (nested, listContexts)++++
+ src/Data/Rewriting/Rules/Ops.hs view
@@ -0,0 +1,108 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini, Bertram Felgenhauer++module Data.Rewriting.Rules.Ops (+    -- * Operations on Rules+    funs,+    funsDL,+    vars,+    varsDL,+    lhss,+    rhss,+    restrictFuns,+    -- * Predicates on Rules+    isLinear, isLeftLinear, isRightLinear,+    isGround, isLeftGround, isRightGround,+    isErasing,+    isCreating,+    isDuplicating,+    isCollapsing,+    isValid,+) where++import Data.Rewriting.Rule (Rule)+import Data.Rewriting.Term (Term)+import qualified Data.Rewriting.Term as Term+import qualified Data.Rewriting.Rule as Rule+++-- | @lhss rs@ returns the list of left-hand sides of @rs@+lhss :: [Rule f v] -> [Term f v]+lhss = 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++-- | Lifting of Term.'Term.funs' to list of rules.+funs :: [Rule f v] -> [f]+funs = flip funsDL []++-- | Difference List version of 'funs'.+-- We have @funsDL r vs = funs r ++ vs@.+funsDL :: [Rule f v] -> [f] -> [f]+funsDL rs fs = foldr Rule.funsDL fs rs++-- | Lifting of Term.'Term.vars' to list of rules.+vars :: [Rule f v] -> [v]+vars = flip varsDL []++-- | Difference List version of 'vars'.+-- We have @varsDL r vs = vars r ++ vs@.+varsDL :: [Rule f v] -> [v] -> [v]+varsDL rs fs = foldr Rule.varsDL fs rs++-- | Returns 'True' iff all given rules satisfy 'Rule.isLinear'+isLinear :: Ord v => [Rule f v] -> Bool+isLinear = all Rule.isLinear++-- | Returns 'True' iff all given rules satisfy 'Rule.isLeftLinear'+isLeftLinear :: Ord v => [Rule f v] -> Bool+isLeftLinear = all Rule.isLeftLinear++-- | Returns 'True' iff all given rules satisfy 'Rule.isRightLinear'+isRightLinear :: Ord v => [Rule f v] -> Bool+isRightLinear = all Rule.isRightLinear++-- | Returns 'True' iff all given rules satisfy 'Rule.isGroundLinear'+isGround :: [Rule f v] -> Bool+isGround = all Rule.isGround++-- | Returns 'True' iff all given rules satisfy 'Rule.isLeftGround'+isLeftGround :: [Rule f v] -> Bool+isLeftGround = all Rule.isLeftGround++-- | Returns 'True' iff all given rules satisfy 'Rule.isRightGround'+isRightGround :: [Rule f v] -> Bool+isRightGround = all Rule.isRightGround++-- | Returns 'True' iff any of the given rules satisfy 'Rule.isErasing'+isErasing :: Ord v => [Rule f v] -> Bool+isErasing = any Rule.isErasing++-- | Returns 'True' iff any of the given rules satisfy 'Rule.isCreating'+isCreating :: Ord v => [Rule f v] -> Bool+isCreating = any Rule.isCreating++-- | Returns 'True' iff any of the given rules satisfy 'Rule.isDuplicating'+isDuplicating :: Ord v => [Rule f v] -> Bool+isDuplicating = any Rule.isDuplicating++-- | Returns 'True' iff any of the given rules satisfy 'Rule.isCollapsing'+isCollapsing :: [Rule f v] -> Bool+isCollapsing = any Rule.isCollapsing++-- | Returns 'True' iff any of the given rules satisfy 'Rule.isExpanding'+isExpanding :: [Rule f v] -> Bool+isExpanding = any Rule.isExpanding++-- | Returns 'True' iff all rules satisfy 'Rule.isValid'+isValid :: Ord v => [Rule f v] -> Bool+isValid = all Rule.isValid++-- | Restrict the rules to those only using function symbols satisfying+-- the given predicate.+restrictFuns :: (f -> Bool) -> [Rule f v] -> [Rule f v]+restrictFuns funp = filter (all funp . Rule.funs)
+ src/Data/Rewriting/Rules/Rewrite.hs view
@@ -0,0 +1,95 @@+-- 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 BangPatterns #-}+-- |+-- Simple rewriting.+--+-- Note: The rules are assumed to be non-creating, i.e., variables on the+-- rhs should also occur on the lhs. Rules violating this constraint+-- will have no effect.+module Data.Rewriting.Rules.Rewrite (+    Reduct (..),+    Strategy,+    fullRewrite,+    outerRewrite,+    innerRewrite,+    rootRewrite,+    -- * utilities not reexported from "Data.Rewriting.Rules"+    nested,+    listContexts,+) where++import Data.Rewriting.Substitution+import Data.Rewriting.Pos+import Data.Rewriting.Rule++import Data.Maybe++-- | A reduct. It contains the resulting term, the position that the term+-- was rewritten at, and the applied rule.+data Reduct f v v' = Reduct {+     result :: Term f v,+     pos :: Pos,+     rule :: Rule f v',+     subst :: GSubst v' f v+}++-- | A rewrite strategy.+type Strategy f v v' = Term f v -> [Reduct f v v']++-- | Full rewriting: Apply rules anywhere in the term.+--+-- Reducts are returned in pre-order: the first is a leftmost, outermost redex.+fullRewrite :: (Ord v', Eq v, Eq f)+    => [Rule f v'] -> Strategy f v v'+fullRewrite trs t = rootRewrite trs t ++ nested (fullRewrite trs) t++-- | Outer rewriting: Apply rules at outermost redexes.+--+-- Reducts are returned in left to right order.+outerRewrite :: (Ord v', Eq v, Eq f)+    => [Rule f v'] -> Strategy f v v'+outerRewrite trs t = case rootRewrite trs t of+    [] -> nested (outerRewrite trs) t+    rs -> rs++-- | Inner rewriting: Apply rules at innermost redexes.+--+-- Reducts are returned in left to right order.+innerRewrite :: (Ord v', Eq v, Eq f)+    => [Rule f v'] -> Strategy f v v'+innerRewrite trs t = case nested (innerRewrite trs) t of+    [] -> rootRewrite trs t+    rs -> rs++-- | Root rewriting: Apply rules only at the root of the term.+--+-- This is mainly useful as a building block for various rewriting strategies.+rootRewrite :: (Ord v', Eq v, Eq f)+    => [Rule f v'] -> Strategy f v v'+rootRewrite trs t = do+    r <- trs+    s <- maybeToList $ match (lhs r) t+    t' <- maybeToList $ gApply s (rhs r)+    return Reduct{ result = t', pos = [], rule = r, subst = s }++-- | Nested rewriting: Apply a rewriting strategy to all arguments of a+-- function symbol, left to right. For variables, the result will be empty.+--+-- This is another building block for rewriting strategies.+nested :: Strategy f v v' -> Strategy f v v'+nested _ (Var _) = []+nested s (Fun f ts) = do+    (n, cl, t) <- listContexts ts+    (\r -> r{ result = Fun f (cl (result r)), pos = n : pos r }) `fmap` s t++-- | Return a list of contexts of a list. Each returned element is an element+-- index (starting from 0), a function that replaces the list element by a+-- new one, and the original element.+listContexts :: [a] -> [(Int, a -> [a], a)]+listContexts = go 0 id where+    go !n f [] = []+    go !n f (x:xs) = (n, f . (: xs), x) : go (n+1) (f . (x:)) xs
+ src/Data/Rewriting/Substitution.hs view
@@ -0,0 +1,27 @@+-- 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, Martin Avanzini++module Data.Rewriting.Substitution (+    GSubst,+    Subst,+    -- * Important operations+    gApply,+    apply,+    compose,+    -- * Reexported modules+    module Data.Rewriting.Substitution.Type,+    module Data.Rewriting.Substitution.Ops,+    module Data.Rewriting.Substitution.Match,+    module Data.Rewriting.Substitution.Unify,+    module Data.Rewriting.Substitution.Pretty,+    module Data.Rewriting.Substitution.Parse,+) where++import Data.Rewriting.Substitution.Type hiding (fromMap, toMap)+import Data.Rewriting.Substitution.Ops+import Data.Rewriting.Substitution.Match+import Data.Rewriting.Substitution.Unify+import Data.Rewriting.Substitution.Pretty+import Data.Rewriting.Substitution.Parse
+ src/Data/Rewriting/Substitution/Match.hs view
@@ -0,0 +1,35 @@+-- 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++module Data.Rewriting.Substitution.Match (+    match,+) where++import Data.Rewriting.Substitution.Type+import qualified Data.Rewriting.Term.Type as Term+import Data.Rewriting.Term.Type (Term (..))++import qualified Data.Map as M+import Control.Monad+import Control.Applicative++-- | Match two terms. If matching succeeds, return the resulting subtitution.+-- We have the following property:+--+-- > match t u == Just s   ==>   apply s t == gapply s t == u+match :: (Eq f, Ord v, Eq v') => Term f v -> Term f v' -> Maybe (GSubst v f v')+match t u = fromMap <$> go t u (M.empty) where+   go (Var v) t subst = case M.lookup v subst of+       Nothing -> Just (M.insert v t subst)+       Just t' | t == t' -> Just subst+       _ -> Nothing+   go (Fun f ts) (Fun f' ts') subst+       | f /= f' || length ts /= length ts' = Nothing+       | otherwise = composeM (zipWith go ts ts') subst+   go _ _ _ = Nothing++-- TODO: move to Utils module+composeM :: Monad m => [a -> m a] -> a -> m a+composeM = foldr (>=>) return
+ src/Data/Rewriting/Substitution/Ops.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, Christian Sternagel++module Data.Rewriting.Substitution.Ops (+    apply,+    gApply,+    compose,+    merge,+) where++import Data.Rewriting.Substitution.Type+import qualified Data.Rewriting.Term.Type as Term+import Data.Rewriting.Term.Type (Term (..))+import qualified Data.Map as M+import Control.Monad+import Control.Applicative++-- | Apply a substitution, assuming that it's the identity on variables not+-- mentionend in the substitution.+apply :: (Ord v) => Subst f v -> Term f v -> Term f v+apply subst = Term.fold var fun where+    var v = M.findWithDefault (Var v) v (toMap subst)+    fun = Fun++-- | Apply a substitution, assuming that it's total. If the term contains+-- a variable not defined by the substitution, return 'Nothing'.+gApply :: (Ord v) => GSubst v f v' -> Term f v -> Maybe (Term f v')+gApply subst = Term.fold var fun where+    var v = M.lookup v (toMap subst)+    fun f ts = Fun f <$> sequence ts++-- | Compose substitutions. We have+--+-- > (s1 `compose` s2) `apply` t = s1 `apply` (s2 `apply` t).+compose :: (Ord v) => Subst f v -> Subst f v -> Subst f v+compose subst subst' =+    fromMap (M.unionWith const (apply subst <$> toMap subst') (toMap subst))++-- | Merge two substitutions. The operation fails if some variable is+-- different terms by the substitutions.+merge :: (Ord v, Eq f, Eq v')+    => GSubst v f v' -> GSubst v f v' -> Maybe (GSubst v f v')+merge subst subst' = do+    guard $ and (M.elems (M.intersectionWith (==) (toMap subst) (toMap subst')))+    return $ fromMap $ M.union (toMap subst) (toMap subst')
+ src/Data/Rewriting/Substitution/Parse.hs view
@@ -0,0 +1,44 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Christian Sternagel++{-# LANGUAGE FlexibleContexts#-}+module Data.Rewriting.Substitution.Parse (+    fromString,+    parse,+    parseIO+) where++import Data.Rewriting.Utils.Parse (ident, lex, par)+import Prelude hiding (lex)+import qualified Data.Map as Map+import Data.Rewriting.Term.Type+import Data.Rewriting.Substitution.Type+import qualified Data.Rewriting.Term.Parse as Term+import Control.Monad+import Text.Parsec hiding (parse)+++parse :: (Ord v) =>+    Parsec String u f -> Parsec String u v -> Parsec String u (Subst f v)+parse fun var = par $ liftM (fromMap . Map.fromList) bindings where+    bindings = binding fun var `sepBy` lex (char ',')+++binding :: Parsec String u f -> Parsec String u v -> Parsec String u (v, Term f v)+binding fun var = liftM2 (,) var (slash >> term) <?> "binding" where+    slash = lex $ char '/'+    term  = Term.parse fun var+++fromString :: [String] -> String -> Either ParseError (Subst String String)+fromString xs = runP (parse fun (var xs)) () "" where+    var = Term.parseVar $ ident "(),{}/" []+    fun = Term.parseFun $ ident "(),{}"  []+++parseIO :: [String] -> String -> IO (Subst String String)+parseIO xs input = case fromString xs input of+    Left err -> do { putStr "parse error at "; print err; mzero }+    Right t  -> return t
+ src/Data/Rewriting/Substitution/Pretty.hs view
@@ -0,0 +1,29 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini++{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}+module Data.Rewriting.Substitution.Pretty (+    prettySubst+) where++import Data.Rewriting.Substitution.Type+import Data.Rewriting.Term (prettyTerm)+import qualified Data.Map as M++import Text.PrettyPrint.ANSI.Leijen++prettyGSubst :: (v -> Doc) -> (f -> Doc) -> (v' -> Doc) -> GSubst v f v' -> Doc+prettyGSubst var fun var' subst =+    encloseSep lbrace rbrace comma [ppBinding v t | (v,t) <- M.toList $ toMap subst]+    where ppBinding v t = var v <> text "/" <> prettyTerm fun var' t++prettySubst :: (f -> Doc) -> (v -> Doc) -> Subst f v -> Doc+prettySubst fun var = prettyGSubst var fun var++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
+ src/Data/Rewriting/Substitution/Type.hs view
@@ -0,0 +1,34 @@+-- 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++module Data.Rewriting.Substitution.Type (+    Subst,+    GSubst,+    -- * utilities not reexported from 'Data.Rewriting.Substitution'+    fromMap,+    toMap,+) where++import Data.Rewriting.Term.Type+import qualified Data.Map as M+++-- | A substitution, mapping variables to terms. Substitutions are+-- equal to the identity almost everywhere.+type Subst f v = GSubst v f v++-- | A generalised? substitution: a finite, partial map from variables+-- to terms with a different variable type.+newtype GSubst v f v' = GS { unGS :: M.Map v (Term f v') }+    deriving Show++-- Do not derive Eq: Depending on the interpretation,  v / Var v+-- will have to be ignored or not.++fromMap :: M.Map v (Term f v') -> GSubst v f v'+fromMap = GS++toMap :: GSubst v f v' -> M.Map v (Term f v')+toMap = unGS
+ src/Data/Rewriting/Substitution/Unify.hs view
@@ -0,0 +1,189 @@+-- 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++module Data.Rewriting.Substitution.Unify (+    unify,+    unifyRef,+) where++import Data.Rewriting.Substitution.Type+import Data.Rewriting.Substitution.Ops (apply)+import qualified Data.Rewriting.Term.Ops as Term+import qualified Data.Rewriting.Term.Type as Term+import Data.Rewriting.Term.Type (Term (..))++import qualified Data.Map as M+import qualified Control.Monad.Union as UM+import qualified Data.Union as U+import Control.Monad.State+import Control.Monad.ST+import Control.Applicative+import Control.Arrow+import Data.Array.ST+import Data.Array+import Data.Maybe+import Data.Word++-- The setup is as follows:+--+-- We have a disjoint set forest, in which every node represents some+-- subterm of our unification problem. Each node is annotated by a+-- description of the term which may refer to other nodes. So we actually+-- have a graph, and an efficient implementation for joining nodes in+-- the graph, curtesy of the union find data structure. We also maintain+-- a map of variables encountered so far to their allocated node.++type UnifyM f v a = StateT (M.Map v U.Node) (UM.UnionM (Annot f v)) a++-- Each node can either represent+-- - a variable (in which case this is the only node representing that variable)+-- - an *expanded* function application with arguments represented by nodes,+-- - or a *pending* function application with normal terms as arguments,+--   not yet represented in the disjoint set forest.++data Annot f v = VarA v | FunA f [U.Node] | FunP f [Term f v]++-- Extract function symbol and arity from (non-variable) annotation.+funari :: Annot f v -> (f, Int)+funari (FunA f ns) = (f, length ns)+funari (FunP f ts) = (f, length ts)++-- Solve a system of equations between terms that are represented by nodes.+solve :: (Eq f, Ord v) => [(U.Node, U.Node)] -> UnifyM f v Bool+solve [] = return True+solve ((t, u) : xs) = do+    (t, t') <- UM.lookup t+    (u, u') <- UM.lookup u+    -- if t == u then the nodes are already equivalent.+    if t == u then solve xs else case (t', u') of+        (VarA _, _) -> do+            -- assign term to variable+            UM.merge (\_ _ -> (u', ())) t u+            solve xs+        (_, VarA _) -> do+            -- assign term to variable+            UM.merge (\_ _ -> (t', ())) t u+            solve xs+        _ | funari t' == funari u' -> do+            -- matching function applications: expand ...+            FunA _ ts <- expand t t'+            FunA _ us <- expand u u'+            UM.merge (\t _ -> (t, ())) t u+            -- ... and equate the argument lists.+            solve (zip ts us ++ xs)+        _ -> do+            -- mismatch, fail.+            return False++-- Expand a node: If the node is currently a pending function application,+-- turn it into an expanded one.+-- The second argument must equal the current annotation of the node.+expand :: (Ord v) => U.Node -> Annot f v -> UnifyM f v (Annot f v)+expand n (FunP f ts) = do+    ann <- FunA f <$> mapM mkNode ts+    UM.annotate n ann+    return ann+expand n ann = return ann++-- Create a new node representing a given term.+-- Variable nodes are shared whenever possible.+-- Function applications will be pending initially.+mkNode :: (Ord v) => Term f v -> UnifyM f v U.Node+mkNode (Var v) = do+    n <- gets (M.lookup v)+    case n of+        Just n -> return n+        Nothing -> do+            n <- UM.new (VarA v)+            modify (M.insert v n)+            return n+mkNode (Fun f ts) = UM.new (FunP f ts)++-- | Unify two terms. If unification succeeds, return a most general unifier+-- of the given terms. We have the following property:+--+-- > unify t u == Just s   ==>   apply s t == apply s u+--+-- /O(n log(n))/, where /n/ is the apparent size of the arguments. Note that+-- the apparent size of the result may be exponential due to shared subterms.+unify :: (Eq f, Ord v) => Term f v -> Term f v -> Maybe (Subst f v)+unify t u = do+    let -- solve unification problem+        act = do+            t' <- mkNode t+            u' <- mkNode u+            success <- solve [(t', u')]+            return (t', success)+        (union, ((root, success), vmap)) = UM.run' $ runStateT act M.empty+        -- find the successors in the resulting graph+        succs n = case snd (U.lookup union n) of+            VarA v -> []+            FunA f ns -> ns+            FunP f ts -> do v <- Term.vars =<< ts; maybeToList (M.lookup v vmap)+    guard $ success && acyclic (U.size union) succs root+    let -- build resulting substitution+        subst = fromMap $ fmap lookupNode vmap+        -- 'terms' maps representatives to their reconstructed terms+        terms = fmap mkTerm (UM.label union)+        -- look up a node in 'terms'+        lookupNode = (terms !) . U.fromNode . fst . U.lookup union+        -- translate annotation back to term+        mkTerm (VarA v) = Var v+        mkTerm (FunA f ns) = Fun f (fmap lookupNode ns)+        mkTerm (FunP f ts) = subst `apply` Fun f ts+    return subst++-- Check whether the subgraph reachable from the given root is acyclic.+-- This is done by a depth first search, where nodes are initially colored+-- white (0), then grey (1) while their children are being visited and+-- finally black (2) after the children have been processed completely.+--+-- The subgraph is cyclic iff we encounter a grey node at some point.+--+-- O(n) plus the cost of 'succs'; 'succs' is called at most once per node.+acyclic :: Int -> (U.Node -> [U.Node]) -> U.Node -> Bool+acyclic size succs root = runST $ do+    let t :: ST s (STUArray s Int Word8)+        t = undefined+    color <- newArray (0, size-1) 0 `asTypeOf` t+    let dfs n = do+            c <- readArray color (U.fromNode n)+            case c of+                0 -> do+                    writeArray color (U.fromNode n) 1+                    flip (foldr andM) (map dfs (succs n)) $ do+                        writeArray color (U.fromNode n) 2+                        return True+                1 -> return False+                2 -> return True+    dfs root++-- monadic, logical and with short-cut evaluation+andM :: Monad m => m Bool -> m Bool -> m Bool+andM a b = do+    a' <- a+    if a' then b else return False++------------------------------------------------------------------------------+-- Reference implementation++-- | Unify two terms. This is a simple implementation for testing purposes,+-- and may be removed in future versions of this library.+unifyRef :: (Eq f, Ord v) => Term f v -> Term f v -> Maybe (Subst f v)+unifyRef t u = fromMap <$> go [(t, u)] M.empty where+   go [] subst = Just subst+   go ((t, u) : xs) subst = case (t, u) of+      (Var v, t) -> add v t xs subst+      (t, Var v) -> add v t xs subst+      (Fun f ts, Fun f' ts')+          | f /= f' || length ts /= length ts' -> Nothing+          | otherwise -> go (zip ts ts' ++ xs) subst+   add v t xs subst+       | Var v == t = go xs subst+       | occurs v t = Nothing+       | otherwise =+           let app = apply (fromMap (M.singleton v t))+           in  go (fmap (app *** app) xs) (M.insert v t (fmap app subst))+   occurs v t = v `elem` Term.vars t
+ src/Data/Rewriting/Term.hs view
@@ -0,0 +1,21 @@+-- 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, Martin Avanzini++module Data.Rewriting.Term (+    Term (..),+    -- * Important operations+    fold, map, vars, funs,+    -- * Reexported modules+    module Data.Rewriting.Term.Type,+    module Data.Rewriting.Term.Ops,+    module Data.Rewriting.Term.Pretty,+    module Data.Rewriting.Term.Parse+) where++import Prelude ()+import Data.Rewriting.Term.Type+import Data.Rewriting.Term.Ops+import Data.Rewriting.Term.Pretty+import Data.Rewriting.Term.Parse
+ src/Data/Rewriting/Term/Ops.hs view
@@ -0,0 +1,110 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Martin Avanzini, Bertram Felgenhauer++module Data.Rewriting.Term.Ops (+    -- * Operations on Terms+    funs,+    funsDL,+    vars,+    varsDL,+    withArity,+    subtermAt,+    replaceAt,+    -- * Predicates on Terms+    isVar,+    isFun,+    isGround,+    isLinear,+    isInstanceOf,+    isVariantOf,+) where++import Data.Rewriting.Pos+import Data.Rewriting.Term.Type as Term+import Data.Rewriting.Substitution.Match+import Data.Maybe+import qualified Data.MultiSet as MS++import Control.Monad (guard)++-- | Annotate each occurrence of a function symbol with its actual arity,+-- i.e., its number of arguments.+--+-- >>> withArity (Fun 'f' [Var 1, Fun 'f' []])+-- Fun ('f',2) [Var 1,Fun ('f',0) []]+withArity :: Term f v -> Term (f, Int) v+withArity = Term.fold Var (\f ts -> Fun (f, length ts) ts)++-- | Return the subterm at a given position.+subtermAt :: Term f v -> Pos -> Maybe (Term f v)+subtermAt t [] = Just t+subtermAt (Fun _ ts) (p:ps) | p >= 0 && p < length ts = subtermAt (ts !! p) ps+subtermAt _ _ = Nothing++-- NOTE: replaceAt and Context.ofTerm have the same recusion structure; is+-- there a nice higher-order function to abstract from it?++-- | replace a subterm at a given position.+replaceAt :: Term f v -> Pos -> Term f v -> Maybe (Term f v)+replaceAt _ [] t' = Just t'+replaceAt (Fun f ts) (i:p) t' = do+    guard (i >= 0 && i < length ts)+    let (ts1, t:ts2) = splitAt i ts+    t <- replaceAt t p t'+    return $ Fun f (ts1 ++ t : ts2)+replaceAt _ _ _ = Nothing++-- | Return the list of all variables in the term, from left to right.+--+-- >>> vars (Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]])+-- [3,1,2,3]+vars :: Term f v -> [v]+vars = flip varsDL []++-- | Difference List version of 'vars'.+-- We have @varsDL t vs = vars t ++ vs@.++varsDL :: Term f v -> [v] -> [v]+varsDL = Term.fold (:) (const $ foldr (.) id)++-- | Return the list of all function symbols in the term, from left to right.+--+-- >>> funs (Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]])+-- "fgf"+funs :: Term f v -> [f]+funs = flip funsDL []++-- | 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)++-- | Return 'True' if the term is a variable, 'False' otherwise.+isVar :: Term f v -> Bool+isVar Var{} = True+isVar Fun{} = False++-- | Return 'True' if the term is a function application, 'False' otherwise.+isFun :: Term f v -> Bool+isFun Var{} = False+isFun Fun{} = True++-- | Check whether the term is a ground term, i.e., contains no variables.+isGround :: Term f v -> Bool+isGround = null . vars++-- | Check whether the term is linear, i.e., contains each variable at most+-- once.+isLinear :: Ord v => Term f v -> Bool+isLinear = all (\(_, c) -> c == 1) . MS.toOccurList . MS.fromList . vars++-- | Check whether a term is an instance of another.+isInstanceOf :: (Eq f, Ord v, Ord v') => Term f v -> Term f v' -> Bool+isInstanceOf t u = isJust (match u t)++-- | 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
+ src/Data/Rewriting/Term/Parse.hs view
@@ -0,0 +1,78 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Christian Sternagel++{-# LANGUAGE FlexibleContexts#-}+module Data.Rewriting.Term.Parse (+    fromString,+    parse,+    parseIO,+    parseFun,+    parseVar,+    parseWST,+) where++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)++-- | Like 'fromString', but the result is wrapped in the IO monad, making this+-- function useful for interactive testing.+--+-- >>> parseIO ["x","y"] "f(x,c)"+-- Fun "f" [Var "x",Fun "c" []]+parseIO :: [String] -> String -> IO (Term String String)+parseIO xs input = case fromString xs input of+    Left err -> do { putStr "parse error at "; print err; mzero }+    Right t  -> return t++-- | @fromString xs s@ parsers a term from the string @s@, where elements of @xs@+-- are considered as variables.+fromString :: [String] -> String -> Either ParseError (Term String String)+fromString xs = runP (parseWST xs) () ""+++-- | @parse fun var@ is a parser for terms, where @fun@ and @var@ are+-- parsers for function symbols and variables, respectively. The @var@ parser+-- has a higher priority than the @fun@ parser. Hence, whenever @var@+-- succeeds, the token is treated as a variable.+--+-- Note that the user has to take care of handling trailing white space in+-- @fun@ and @var@.+parse :: Stream s m Char => ParsecT s u m f -> ParsecT s u m v+    -> ParsecT s u m (Term f v)+parse fun var = term <?> "term" where+    term = try (liftM Var var) <|> liftM2 Fun fun args+    args =  par (sepBy term (lex $ char ',')) <|> return []+++-- | @parseWST xs@ is a parser for terms following the conventions of the+-- ancient ASCII input format of the termination competition: every @Char@ that+-- is neither a white space (according to 'Data.Char.isSpace') nor one of '@(@',+-- '@)@', or '@,@', is considered a letter. An identifier is a non-empty+-- sequence of letters and it is treated as variable iff it is contained in+-- @xs@.++-- change name?+parseWST :: Stream s m Char => [String] -> ParsecT s u m (Term String String)+parseWST xs = parse (parseFun identWST) (parseVar identWST xs)++-- | @parseFun ident@ parses function symbols defined by @ident@.+parseFun :: Stream s m Char => ParsecT s u m String -> ParsecT s u m String+parseFun id = lex id <?> "function symbol"++-- | @parseVar ident vars@ parses variables as defined by @ident@ and with the+-- additional requirement that the result is a member of @vars@.+parseVar :: Stream s m Char =>+    ParsecT s u m String -> [String] -> ParsecT s u m String+parseVar id xs =  do { x <- lex id; guard (x `elem` xs); return x }+              <?> "variable"++identWST :: Stream s m Char => ParsecT s u m String+-- COMMENT: according to http://www.lri.fr/~marche/tpdb/format.html '"' and some+-- reserved strings are also not allowed, but I don't see the point+identWST = ident "()," []
+ src/Data/Rewriting/Term/Pretty.hs view
@@ -0,0 +1,22 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Auhtors: Martin Avanzini, Christian Sternagel++module Data.Rewriting.Term.Pretty (+    prettyTerm,+) where++import Data.Rewriting.Term.Type+import Text.PrettyPrint.ANSI.Leijen++-- | Given a pretty printer @f@ for function symbols and pretty printer @v@ for variables+-- @prettyTerm f v@ produces a pretty printer for terms++prettyTerm :: (f -> Doc) -> (v -> Doc) -> Term f v -> Doc+prettyTerm _         var (Var x) = var x+prettyTerm fun var (Fun f ts)    = fun f <> args where+    args = encloseSep lparen rparen comma [prettyTerm fun var ti | ti <- ts]++instance (Pretty f, Pretty v) => Pretty (Term f v) where+    pretty = prettyTerm pretty pretty
+ src/Data/Rewriting/Term/Type.hs view
@@ -0,0 +1,32 @@+-- 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++module Data.Rewriting.Term.Type (+    Term (..),+    fold,+    map,+) where++import Prelude hiding (map)++data Term f v+    = Var v            -- ^ Variable+    | Fun f [Term f v] -- ^ Function application+    deriving (Show, Eq, Ord)++-- | Folding terms.+--+-- >>> fold (\v -> 1) (\f xs -> 1 + sum xs) (Fun 'f' [Var 1, Fun 'g' []])+-- 3 -- size of the given term+fold :: (v -> a) -> (f -> [a] -> a) -> Term f v -> a+fold var fun (Var v) = var v+fold var fun (Fun f ts) = fun f (fmap (fold var fun) ts)++-- | Mapping terms: Rename function symbols and variables.+--+-- >>> map succ pred (Fun 'f' [Var 2, Fun 'g' []])+-- Fun 'e' [Var 3,Fun 'f' []]+map :: (f -> f') -> (v -> v') -> Term f v -> Term f' v'+map fun var = fold (Var . var) (Fun . fun)
+ src/Data/Rewriting/Utils.hs view
@@ -0,0 +1,17 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Christian Sternagel++module Data.Rewriting.Utils (+    dropCommonPrefix,+) where++-- | @dropCommonPrefix xs ys@ removes the common prefix of @xs@ and @ys@ and+-- returns the remaining lists as a pair.+--+-- >>>dropCommonPrefix [1,2,3] [1,2,4,1]+-- ([3], [4,1])+dropCommonPrefix :: Ord a => [a] -> [a] -> ([a], [a])+dropCommonPrefix (x:xs) (y:ys) | x == y = dropCommonPrefix xs ys+dropCommonPrefix   xs     ys            = (xs, ys)
+ src/Data/Rewriting/Utils/Parse.hs view
@@ -0,0 +1,32 @@+-- This file is part of the 'term-rewriting' library. It is licensed+-- under an MIT license. See the accompanying 'LICENSE' file for details.+--+-- Authors: Christian Sternagel++{-# LANGUAGE FlexibleContexts#-}+module Data.Rewriting.Utils.Parse (+    lex,+    par,+    ident+) where++import Control.Monad+import Prelude hiding (lex)+import Text.Parsec+import Data.Char (isSpace)++-- | @lex p@ is similar to @p@ but also consumes trailing white space.+lex :: Stream s m Char => ParsecT s u m a -> ParsecT s u m a+lex p = do { x <- p; spaces; return x }++-- | @par p@ accpets @p@ enclosed in parentheses ('@(@' and '@)@').+par :: Stream s m Char => ParsecT s u m a -> ParsecT s u m a+par = between (lex$char '(') (lex$char ')')++-- | @ident taboo@ parses a non-empty sequence of non-space characters not+-- containing elements of @taboo@.+ident :: Stream s m Char => String -> [String] -> ParsecT s u m String+ident tabooChars tabooWords = try $ do+    s <- many1 (satisfy (\c -> not (isSpace c) && c `notElem` tabooChars))+    guard (s `notElem` tabooWords)+    return s
+ term-rewriting.cabal view
@@ -0,0 +1,73 @@+name:          term-rewriting+version:       0.1+stability:     experimental+author:        Martin Avanzini,+               Bertram Felgenhauer,+               Christian Sternagel+homepage:      http://cl-informatik.uibk.ac.at/software/haskell-rewriting/+maintainer:    haskell-rewriting@informatik.uibk.ac.at+license:       MIT+license-file:  LICENSE+category:      Logic+synopsis:      Term Rewriting Library+description:   +  Yet Another Term Rewriting Library.+  .+  This library provides basic data types and functionality for first order+  term rewriting.+build-type:    Simple+cabal-version: >= 1.6++source-repository head+    type: git+    location: git://github.com/haskell-rewriting/term-rewriting++library+    hs-source-dirs:+        src+    exposed-modules:+        Data.Rewriting.Term+        Data.Rewriting.Term.Type+        Data.Rewriting.Term.Ops +        Data.Rewriting.Term.Parse+        Data.Rewriting.Term.Pretty+        Data.Rewriting.Pos+        Data.Rewriting.Problem+        Data.Rewriting.Problem.Type+        Data.Rewriting.Problem.Parse+        Data.Rewriting.Problem.Pretty+        Data.Rewriting.Rule+        Data.Rewriting.Rule.Type+        Data.Rewriting.Rule.Pretty+        Data.Rewriting.Rule.Ops+        Data.Rewriting.Substitution+        Data.Rewriting.Substitution.Type+        Data.Rewriting.Substitution.Parse+        Data.Rewriting.Substitution.Ops+        Data.Rewriting.Substitution.Pretty+        Data.Rewriting.Substitution.Match+        Data.Rewriting.Substitution.Unify+        Data.Rewriting.Rules+        Data.Rewriting.Rules.Rewrite+        Data.Rewriting.Rules.Ops+        Data.Rewriting.Context+        Data.Rewriting.Context.Type+        Data.Rewriting.Context.Ops+        Data.Rewriting.CriticalPair+        Data.Rewriting.CriticalPair.Type+        Data.Rewriting.CriticalPair.Ops+    other-modules:+        Data.Rewriting.Utils+        Data.Rewriting.Utils.Parse+    build-depends:+        containers >= 0.3 && < 0.6,+        multiset >= 0.2 && < 0.3,+        parsec >= 3 && < 3.2,+        union-find-array >= 0.1 && < 0.2,+        array >= 0.3 && < 0.5,+        ansi-wl-pprint >= 0.6 && < 0.7,+        mtl >= 1.1 && < 2.2,+        base >= 4 && < 5+    extensions:+        TypeSynonymInstances+        BangPatterns