diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#! /usr/bin/env runghc
+> import Distribution.Simple (defaultMain)
+> main = defaultMain
diff --git a/src/Data/Rewriting/Context.hs b/src/Data/Rewriting/Context.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Context.hs
@@ -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
diff --git a/src/Data/Rewriting/Context/Ops.hs b/src/Data/Rewriting/Context/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Context/Ops.hs
@@ -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
diff --git a/src/Data/Rewriting/Context/Type.hs b/src/Data/Rewriting/Context/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Context/Type.hs
@@ -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)
diff --git a/src/Data/Rewriting/CriticalPair.hs b/src/Data/Rewriting/CriticalPair.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/CriticalPair.hs
@@ -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
diff --git a/src/Data/Rewriting/CriticalPair/Ops.hs b/src/Data/Rewriting/CriticalPair/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/CriticalPair/Ops.hs
@@ -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
diff --git a/src/Data/Rewriting/CriticalPair/Type.hs b/src/Data/Rewriting/CriticalPair/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/CriticalPair/Type.hs
@@ -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
+}
diff --git a/src/Data/Rewriting/Pos.hs b/src/Data/Rewriting/Pos.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Pos.hs
@@ -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)
diff --git a/src/Data/Rewriting/Problem.hs b/src/Data/Rewriting/Problem.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Problem.hs
@@ -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
diff --git a/src/Data/Rewriting/Problem/Parse.hs b/src/Data/Rewriting/Problem/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Problem/Parse.hs
@@ -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
diff --git a/src/Data/Rewriting/Problem/Pretty.hs b/src/Data/Rewriting/Problem/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Problem/Pretty.hs
@@ -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
diff --git a/src/Data/Rewriting/Problem/Type.hs b/src/Data/Rewriting/Problem/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Problem/Type.hs
@@ -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
diff --git a/src/Data/Rewriting/Rule.hs b/src/Data/Rewriting/Rule.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rule.hs
@@ -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
diff --git a/src/Data/Rewriting/Rule/Ops.hs b/src/Data/Rewriting/Rule/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rule/Ops.hs
@@ -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
diff --git a/src/Data/Rewriting/Rule/Pretty.hs b/src/Data/Rewriting/Rule/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rule/Pretty.hs
@@ -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
+
diff --git a/src/Data/Rewriting/Rule/Type.hs b/src/Data/Rewriting/Rule/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rule/Type.hs
@@ -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) }
+
diff --git a/src/Data/Rewriting/Rules.hs b/src/Data/Rewriting/Rules.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rules.hs
@@ -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)
+
+
+
+
diff --git a/src/Data/Rewriting/Rules/Ops.hs b/src/Data/Rewriting/Rules/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rules/Ops.hs
@@ -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)
diff --git a/src/Data/Rewriting/Rules/Rewrite.hs b/src/Data/Rewriting/Rules/Rewrite.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Rules/Rewrite.hs
@@ -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
diff --git a/src/Data/Rewriting/Substitution.hs b/src/Data/Rewriting/Substitution.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Substitution.hs
@@ -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
diff --git a/src/Data/Rewriting/Substitution/Match.hs b/src/Data/Rewriting/Substitution/Match.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Substitution/Match.hs
@@ -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
diff --git a/src/Data/Rewriting/Substitution/Ops.hs b/src/Data/Rewriting/Substitution/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Substitution/Ops.hs
@@ -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')
diff --git a/src/Data/Rewriting/Substitution/Parse.hs b/src/Data/Rewriting/Substitution/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Substitution/Parse.hs
@@ -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
diff --git a/src/Data/Rewriting/Substitution/Pretty.hs b/src/Data/Rewriting/Substitution/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Substitution/Pretty.hs
@@ -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
diff --git a/src/Data/Rewriting/Substitution/Type.hs b/src/Data/Rewriting/Substitution/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Substitution/Type.hs
@@ -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
diff --git a/src/Data/Rewriting/Substitution/Unify.hs b/src/Data/Rewriting/Substitution/Unify.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Substitution/Unify.hs
@@ -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
diff --git a/src/Data/Rewriting/Term.hs b/src/Data/Rewriting/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Term.hs
@@ -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
diff --git a/src/Data/Rewriting/Term/Ops.hs b/src/Data/Rewriting/Term/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Term/Ops.hs
@@ -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
diff --git a/src/Data/Rewriting/Term/Parse.hs b/src/Data/Rewriting/Term/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Term/Parse.hs
@@ -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 "()," []
diff --git a/src/Data/Rewriting/Term/Pretty.hs b/src/Data/Rewriting/Term/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Term/Pretty.hs
@@ -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
diff --git a/src/Data/Rewriting/Term/Type.hs b/src/Data/Rewriting/Term/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Term/Type.hs
@@ -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)
diff --git a/src/Data/Rewriting/Utils.hs b/src/Data/Rewriting/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Utils.hs
@@ -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)
diff --git a/src/Data/Rewriting/Utils/Parse.hs b/src/Data/Rewriting/Utils/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Rewriting/Utils/Parse.hs
@@ -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
diff --git a/term-rewriting.cabal b/term-rewriting.cabal
new file mode 100644
--- /dev/null
+++ b/term-rewriting.cabal
@@ -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