diff --git a/TPDB/CPF/Proof/Read.hs b/TPDB/CPF/Proof/Read.hs
deleted file mode 100644
--- a/TPDB/CPF/Proof/Read.hs
+++ /dev/null
@@ -1,117 +0,0 @@
-{-# language Arrows, NoMonomorphismRestriction, PatternSignatures #-}
-
-module TPDB.CPF.Proof.Read where
-
-import TPDB.CPF.Proof.Type 
-import TPDB.Data
-
-import Text.XML.HXT.Arrow.XmlArrow
-
-import Text.XML.HXT.Arrow.XmlState ( runX )
-import Text.XML.HXT.Arrow.ReadDocument ( readString )
-import Text.XML.HXT.Arrow.XmlOptions ( a_validate )
-import Text.XML.HXT.DOM.XmlKeywords (v_0)
-import Control.Arrow
-import Control.Arrow.ArrowList
-import Control.Arrow.ArrowTree
-
-import qualified TPDB.CPF.Proof.Write as W -- for testing
-import qualified Text.XML.HXT.Arrow.XmlState as X 
-
-{- | dangerous: 
-not all constructor arguments will be set.
-the function produces something like
-
-      CertificationProblem { input = CertificationProblemInput 
-                          , proof = TrsTerminationProof undefined
-                          }  
--}
-
-readCP :: String -> IO [ CertificationProblem ]
-readCP = readCP_with_tracelevel 0
-
-readCP_with_tracelevel l s = runX ( X.withTraceLevel l $ readString [] s >>> getCP )
-
-getCP = getChild "certificationProblem" >>> proc x -> do
-    inp <- getInput <<< getChild "input" -< x
-    pro <- getProof <<< getChild "proof" -< x
-    ver <- getText <<< gotoChild "cpfVersion" -< x
-    returnA -< CertificationProblem 
-        { input = inp, proof = pro, cpfVersion = ver, origin = ignoredOrigin }
-
-getInput = getTerminationInput <+> getComplexityInput
-
-getTerminationInput = hasName "input" >>> proc x -> do
-    trsI <- getTrsInput <<< getChild "trsInput" -< x    
-    returnA -< TrsInput $ RS { rules = trsI, separate = False }
-
-getComplexityInput = hasName "input" >>> proc x -> do
-    y <- getChild "complexityInput" -< x
-    trsI <- getTrsInput <<< getChild "trsInput" -< y
-    cm <- getComplexityMeasure -< y
-    cc <- getComplexityClass -< y
-    returnA -< ComplexityInput
-        { trsinput_trs = RS { rules = trsI, separate = False }
-        , complexityMeasure = cm
-        , complexityClass = cc
-        }
-
-getComplexityMeasure = 
-        getDummy "derivationalComplexity" DerivationalComplexity
-    <+> getDummy "runtimeComplexity" RuntimeComplexity
-
-getComplexityClass = proc x -> do
-    d <- getText <<< gotoChild "polynomial" -< x
-    returnA -< ComplexityClassPolynomial { degree = read d }
-
-getTrsInput = proc x -> do
-    sys <- getTrs <<< getChild "trs" -< x
-    rels <- listA ( getTrsWith Weak <<< getChild "relativeRules" ) -< x
-    returnA -< sys ++ concat rels
-
-getTrs = getTrsWith Strict
-
-getTrsWith s = proc x -> do
-    str <- getRules s <<< getChild "rules" -< x
-    returnA -< str
-
-getProof = getDummy "trsTerminationProof" ( TrsTerminationProof undefined )
-       <+> getDummy "trsNonterminationProof" ( TrsNonterminationProof undefined )
-       <+> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined )
-       <+> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined )
-       <+> getDummy "complexityProof" ( ComplexityProof undefined )
-
-getDummy t c = proc x -> do 
-    getChild t -< x
-    returnA -< c 
-
-getRules str = proc x -> do
-    returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x
-
-getRule str = proc x -> do
-    l <-  getTerm <<< isElem <<< gotoChild "lhs" -< x
-    r <-  getTerm <<< isElem <<< gotoChild "rhs" -< x
-    returnA -< Rule { lhs = l, relation = str, rhs = r, top = False }
-
-
-getTerm = getVar <+> getFunApp
-
-getVar = proc x -> do
-    nm <- getText <<< getChildren <<< hasName "var" -< x
-    returnA -< Var $ mk 0 nm
-
-getFunApp = proc x -> do
-    sub <- hasName "funapp" -< x
-    nm <- getText <<< gotoChild "name" -< sub
-    gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub
-    let c = mk (length gs) nm
-    returnA -< Node c gs
-          
-gotoChild tag = proc x -> do
-    returnA <<< getChildren <<< getChild tag -< x
-
-getChild tag = proc x -> do
-    returnA <<< hasName tag <<< isElem <<< getChildren -< x
-
-
-
diff --git a/TPDB/CPF/Proof/Type.hs b/TPDB/CPF/Proof/Type.hs
deleted file mode 100644
--- a/TPDB/CPF/Proof/Type.hs
+++ /dev/null
@@ -1,215 +0,0 @@
-{-# language StandaloneDeriving #-}
-{-# language ExistentialQuantification #-}
-{-# language DeriveDataTypeable #-}
-
--- | internal representation of CPF termination proofs,
--- see <http://cl-informatik.uibk.ac.at/software/cpf/>
-
-module TPDB.CPF.Proof.Type 
-
-( module TPDB.CPF.Proof.Type
-, Identifier
-, TES
-)
-
-where
-
-import TPDB.Data
-import Data.Typeable
-
-import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
-
-data CertificationProblem =
-     CertificationProblem { input :: CertificationProblemInput 
-                          , cpfVersion :: String -- urgh
-                          , proof :: Proof 
-                          , origin :: Origin  
-                          }  
-   deriving ( Typeable, Eq )
-
-data Origin = ProofOrigin { tool :: Tool }
-    deriving ( Typeable, Eq )
-
-ignoredOrigin = ProofOrigin { tool = Tool "ignored" "ignored"  }
-
-data Tool = Tool { name :: String 
-                 , version :: String
-                 } 
-    deriving ( Typeable, Eq )
-
-data CertificationProblemInput 
-    = TrsInput { trsinput_trs :: TRS Identifier Identifier }
-      -- ^ this is actually not true, since instead of copying from XTC,
-      -- CPF format repeats the definition of TRS,
-      -- and it's a different one (relative rules are extra)
-    | ComplexityInput { trsinput_trs :: TRS Identifier Identifier
-                      , complexityMeasure :: ComplexityMeasure
-                      , complexityClass :: ComplexityClass      
-                      }
-   deriving ( Typeable, Eq )      
-
-data Proof = TrsTerminationProof TrsTerminationProof
-           | TrsNonterminationProof TrsNonterminationProof
-           | RelativeTerminationProof TrsTerminationProof
-           | RelativeNonterminationProof TrsNonterminationProof
-           | ComplexityProof ComplexityProof
-   deriving ( Typeable, Eq )
-
-data DPS = forall s . ( XmlContent s , Typeable s, Eq s ) 
-        => DPS [ Rule (Term Identifier s) ]
-   deriving ( Typeable )
-
-instance Eq DPS where x == y = error "instance Eq DPS"
-
-
-data ComplexityProof = ComplexityProofFIXME ()
-    deriving ( Typeable, Eq )
-
-data ComplexityMeasure 
-     = DerivationalComplexity
-     | RuntimeComplexity
-    deriving ( Typeable, Eq )
-
-data ComplexityClass = 
-     ComplexityClassPolynomial { degree :: Int } 
-     -- ^ it seems the degree must always be given in CPF,
-     -- although the category spec also allows "POLY"
-     -- http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php
-    deriving ( Typeable, Eq )
-
-data TrsNonterminationProof = TrsNonterminationProofFIXME ()
-    deriving ( Typeable, Eq )
-
-data TrsTerminationProof 
-     = RIsEmpty
-     | RuleRemoval { rr_orderingConstraintProof :: OrderingConstraintProof
-                   , trs :: TRS Identifier Identifier 
-                   , trsTerminationProof :: TrsTerminationProof  
-                   }  
-     | DpTrans  { dptrans_dps :: DPS
-                , markedSymbols :: Bool , dptrans_dpProof :: DpProof }
-     | Semlab {  model :: Model 
-              , trs :: TRS Identifier Identifier
-              , trsTerminationProof :: TrsTerminationProof
-              }
-     | Unlab {  trs :: TRS Identifier Identifier
-              , trsTerminationProof :: TrsTerminationProof
-              }
-     | StringReversal { trs :: TRS Identifier Identifier
-                      , trsTerminationProof :: TrsTerminationProof  
-                      }  
-   deriving ( Typeable, Eq )
-
-data Model = FiniteModel Int [Interpret]
-   deriving ( Typeable, Eq )
-       
-data DpProof = PIsEmpty  
-             | RedPairProc { rppOrderingConstraintProof :: OrderingConstraintProof
-                           , rppDps                     :: DPS 
-                           , rppUsableRules             :: Maybe DPS
-                           , rppDpProof                 :: DpProof 
-                           }  
-             | DepGraphProc [ DepGraphComponent ]
-
-             | SemLabProc { slpModel   :: Model
-                          , slpDps     :: DPS
-                          , slpTrs     :: DPS
-                          , slpDpProof :: DpProof
-                          }
-             | UnlabProc  { ulpDps :: DPS
-                          , ulpTrs :: DPS
-                          , ulpDpProof :: DpProof
-                          }
-   deriving ( Typeable, Eq )
-
-data DepGraphComponent =
-     DepGraphComponent { dgcRealScc :: Bool
-                       , dgcDps :: DPS
-                       , dgcDpProof :: DpProof
-                       }
-   deriving ( Typeable, Eq )
-
-data OrderingConstraintProof = OCPRedPair RedPair
-                             deriving ( Typeable, Eq )
-
-data RedPair = RPInterpretation Interpretation
-             | RPPathOrder      PathOrder
-             deriving ( Typeable, Eq )
-
-data Interpretation =
-     Interpretation { interpretation_type :: Interpretation_Type
-                    , interprets :: [ Interpret  ]
-                    }
-   deriving ( Typeable, Eq )
-
-data Interpretation_Type = 
-   Matrix_Interpretation { domain :: Domain, dimension :: Int
-                         , strictDimension :: Int
-                         }
-   deriving ( Typeable, Eq )
-
-data Domain = Naturals 
-            | Rationals Rational
-            | Arctic Domain
-            | Tropical Domain
-   deriving ( Typeable, Eq )
-
-data Interpret = Interpret 
-    { symbol :: Symbol , arity :: Int , value :: Value }
-   deriving ( Typeable, Eq )
-
-data Value = Polynomial    Polynomial
-           | ArithFunction ArithFunction
-   deriving ( Typeable, Eq )
-
-data Polynomial = Sum [ Polynomial ]
-                | Product [ Polynomial ]
-                | Polynomial_Coefficient Coefficient
-                | Polynomial_Variable String
-   deriving ( Typeable, Eq )
-
-data ArithFunction = AFNatural  Integer
-                   | AFVariable Integer
-                   | AFSum      [ArithFunction]
-                   | AFProduct  [ArithFunction]
-                   | AFMin      [ArithFunction]
-                   | AFMax      [ArithFunction]
-                   | AFIfEqual  ArithFunction ArithFunction ArithFunction ArithFunction
-                   deriving ( Typeable, Eq )
-
-data Symbol = SymName  Identifier
-            | SymSharp Symbol
-            | SymLabel Symbol Label
-            deriving ( Typeable, Eq )
-
-data Label = LblNumber [Integer]
-           | LblSymbol [Symbol]
-           deriving ( Typeable, Eq )
-
-data Coefficient = Vector [ Coefficient ]
-           | Matrix [ Coefficient ]
-           | forall a . (Eq a, XmlContent a ) => Coefficient_Coefficient a
-   deriving ( Typeable )
-
-instance Eq Coefficient where x == y = error "instance Eq Coefficient"
-
-data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite
-   deriving ( Typeable, Eq )
-
-class ToExotic a where toExotic :: a -> Exotic
-
-data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
-               deriving ( Typeable, Eq )
-
-data PrecedenceEntry = PrecedenceEntry { peSymbol     :: Symbol
-                                       , peArity      :: Int
-                                       , pePrecedence :: Integer
-                                       }
-                     deriving ( Typeable, Eq )
-
-data ArgumentFilterEntry = 
-     ArgumentFilterEntry { afeSymbol :: Symbol
-                         , afeArity  :: Int
-                         , afeFilter :: Either Int [Int]
-                         }
-     deriving ( Typeable, Eq )
diff --git a/TPDB/CPF/Proof/Util.hs b/TPDB/CPF/Proof/Util.hs
deleted file mode 100644
--- a/TPDB/CPF/Proof/Util.hs
+++ /dev/null
@@ -1,26 +0,0 @@
-{-# LANGUAGE LambdaCase #-}
-module TPDB.CPF.Proof.Util where
-
-import qualified Data.Map as M
-import           Data.List (nub)
-import           TPDB.Data 
-import           TPDB.CPF.Proof.Type hiding (name)
-import           TPDB.DP 
-
-fromMarkedIdentifier :: Marked Identifier -> Symbol
-fromMarkedIdentifier = \case 
-  Original i -> SymName i
-  Marked i   -> SymSharp $ SymName i
-
-sortVariables :: Rule (Term Identifier s) -> Rule (Term Identifier s)
-sortVariables r = r { lhs = vmap mapVar $ lhs r
-                    , rhs = vmap mapVar $ rhs r
-                    }
-  where
-    oldVars      = nub $ voccs $ lhs r
-    newVars      = zipWith mkNewVar [1..] oldVars
-    mkNewVar i v = v { name = "x" ++ show i }
-    mapping      = M.fromList $ zip oldVars newVars
-    mapVar v     = case M.lookup v mapping of
-      Just v' -> v'
-      Nothing -> error "TPDB.CPF.Proof.Util.sortVariables"
diff --git a/TPDB/CPF/Proof/Write.hs b/TPDB/CPF/Proof/Write.hs
deleted file mode 100644
--- a/TPDB/CPF/Proof/Write.hs
+++ /dev/null
@@ -1,333 +0,0 @@
-{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}
-
--- | from internal representation to XML, and back
-
-module TPDB.CPF.Proof.Write where
-
-import TPDB.CPF.Proof.Type
-import qualified TPDB.Data as T
-
-import qualified Text.XML.HaXml.Escape as E
-import qualified Text.XML.HaXml.Pretty as P
-
-import Text.XML.HaXml.Types (QName (..) )
-import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
-import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..), Misc (PI) )
-
-import TPDB.Xml 
-import TPDB.Data.Xml 
-
-import Data.List ( nub )
-import Data.Char ( toLower )
-import Data.Map (Map)
-import qualified Data.Map as Map
-
-import qualified Data.Time as T
-import Control.Monad
-import Data.Typeable
-import Data.Ratio
-
-tox :: CertificationProblem -> Document ()
-tox p = 
-    let xd = XMLDecl "1.0" ( Just $ EncodingDecl "UTF-8" ) Nothing 
-        style = PI ("xml-stylesheet", "type=\"text/xsl\" href=\"cpfHTML.xsl\"")
-        pro = Prolog ( Just xd ) [] Nothing [style]
-        [ CElem e _ ] = toContents p
-    in  Document pro emptyST e []
-
-instance XmlContent CertificationProblem where
-   parseContents = error "parseContents not implemented"
-
-   toContents cp = rmkel "certificationProblem"
-         [ mkel "input" $ toContents ( input cp )
-         , mkel "cpfVersion" [ nospaceString $ cpfVersion cp ]
-         , mkel "proof" $ toContents ( proof cp )
-         , mkel "origin" $ toContents ( origin cp )
-         ]
-
-instance XmlContent Origin where
-   parseContents = error "parseContents not implemented"
-
-   toContents o = case o of
-       ProofOrigin t -> rmkel "proofOrigin" $ toContents t
-
-instance XmlContent Tool where
-   parseContents = error "parseContents not implemented"
-
-   toContents t = rmkel "tool" 
-         [ mkel "name"    [ nospaceString $ name    t ]
-         , mkel "version" [ nospaceString $ version t ]
-         ]
-
-instance XmlContent CertificationProblemInput where
-   parseContents = error "parseContents not implemented"
-
-   toContents i = case i of
-      TrsInput {} -> rmkel "trsInput" $ toContents ( symbolize $ trsinput_trs i )
-      ComplexityInput {} -> rmkel "complexityInput" $ concat
-          [ rmkel "trsInput" $ toContents $ symbolize $ trsinput_trs i
-          ]
-
-instance XmlContent ( T.TRS Identifier Symbol ) where
-   parseContents = error "parseContents not implemented"
-
-   toContents s = rmkel "trs" 
-       $ rmkel "rules" $ concat $ map toContents $ T.rules s
-
-instance ( Typeable t, XmlContent t  ) 
-        => XmlContent ( T.Rule t) where
-   parseContents = error "parseContents not implemented"
-
-   toContents u = rmkel "rule" $ concat
-      [ rmkel "lhs" ( toContents $ T.lhs u )
-      , rmkel "rhs" ( toContents $ T.rhs u )
-      ]
-
-instance XmlContent Proof where
-   parseContents = error "parseContents not implemented"
-
-   toContents p = 
-     let missing t = rmkel t $ rmkel "missing-toContents-instance" [] 
-     in  case p of
-       TrsTerminationProof p -> toContents p
-       TrsNonterminationProof p -> missing "TrsNonterminationProof"
-       RelativeTerminationProof p -> missing "RelativeTerminationProof"
-       RelativeNonterminationProof p -> missing "RelativeNonterminationProof"
-       ComplexityProof p -> missing "ComplexityProof"
-
-instance XmlContent DPS where
-   parseContents = error "parseContents not implemented"
-
-   toContents ( DPS rules ) = rmkel "dps" 
-        $ rmkel "rules" $ rules >>= toContents
-
-instance XmlContent TrsTerminationProof where
-   parseContents = error "parseContents not implemented"
-
-   toContents p = rmkel "trsTerminationProof" $ case p of
-      RIsEmpty -> rmkel "rIsEmpty" []
-      DpTrans {} -> rmkel "dpTrans" $ concat
-          [ toContents $ dptrans_dps p
-          , rmkel "markedSymbols" [ nospaceString "true" ]
-          , toContents $ dptrans_dpProof p
-          ]
-      StringReversal {} -> rmkel "stringReversal" $ concat
-          [ toContents $ symbolize $ trs p
-          , toContents $ trsTerminationProof p
-          ]
-      RuleRemoval {} -> rmkel "ruleRemoval" $ concat
-          [ toContents $ rr_orderingConstraintProof p
-          , toContents $ symbolize $ trs p
-          , toContents $ trsTerminationProof p
-          ]
-
-symbolize trs = 
-    ( fmap (fmap SymName) trs )
-    { T.signature = map SymName $ T.signature trs }
-
-instance XmlContent Model where
-  parseContents = error "parseContents not implemented"
-
-  toContents model = rmkel "model" $ case model of
-    FiniteModel carrierSize interprets ->
-      rmkel "finiteModel" $ concat
-        [ rmkel "carrierSize" [ nospaceString $ show carrierSize ]
-        , concatMap toContents interprets
-        ]
-
-instance XmlContent DpProof where
-  parseContents = error "parseContents not implemented"
-
-  toContents p = rmkel "dpProof" $ case p of
-    PIsEmpty -> rmkel "pIsEmpty" []
-    RedPairProc {} -> case rppUsableRules p of
-      Nothing -> rmkel "redPairProc" $ concat
-        [ toContents $ rppOrderingConstraintProof p
-        , toContents $ rppDps p
-        , toContents $ rppDpProof p
-        ]
-      Just (DPS ur) -> rmkel "redPairUrProc" $ concat
-        [ toContents $ rppOrderingConstraintProof p
-        , toContents $ rppDps p
-        , rmkel "usableRules" $ rmkel "rules" $ concatMap toContents ur
-        , toContents $ rppDpProof p
-        ]
-    DepGraphProc cs -> rmkel "depGraphProc" $ concat $ map toContents cs
-
-    SemLabProc {} -> rmkel "semlabProc" $ concat
-      [ toContents $ slpModel p
-      , toContents $ slpDps p
-      , case slpTrs p of
-          DPS rules -> rmkel "trs" $ rmkel "rules" $ rules >>= toContents
-
-      , toContents $ slpDpProof p
-      ]
-
-    UnlabProc {} -> rmkel "unlabProc" $ concat
-      [ toContents $ ulpDps p
-      , case ulpTrs p of
-          DPS rules -> rmkel "trs" $ rmkel "rules" $ rules >>= toContents
-      , toContents $ ulpDpProof p
-      ]
-
-instance XmlContent DepGraphComponent where
-    toContents dgc = rmkel "component" $ concat $
-        [ {- rmkel "dps" $ -} toContents $ dgcDps dgc
-        , rmkel "realScc" 
-           --  $ toContents $ dgcRealScc dgc
-           -- NO, Bool is encoded as text, not as attribute
-            [ nospaceString $ map toLower $ show $ dgcRealScc dgc ]
-        ] ++ 
-        [ {- rmkel "dpProof" $ -} toContents $ dgcDpProof dgc
-        | dgcRealScc dgc
-        ]
-
-instance XmlContent OrderingConstraintProof where
-  parseContents = error "parseContents not implemented"
-
-  toContents (OCPRedPair rp) = rmkel "orderingConstraintProof" 
-                             $ toContents rp
-           
-instance XmlContent RedPair where
-  parseContents = error "parseContents not implemented"
-
-  toContents rp = rmkel "redPair" $ case rp of
-    RPInterpretation i -> toContents i
-    RPPathOrder      o -> toContents o
-
-instance XmlContent Interpretation where
-   parseContents = error "parseContents not implemented"
-
-   toContents i = rmkel "interpretation" $
-        rmkel "type" ( toContents $ interpretation_type i )
-     ++ concatMap toContents ( interprets i )
-      
-instance XmlContent Interpretation_Type where
-   parseContents = error "parseContents not implemented"
-
-   toContents t = rmkel "matrixInterpretation" $ concat 
-      [ toContents ( domain t )
-      , rmkel "dimension"       [ nospaceString $ show $ dimension t ]
-      , rmkel "strictDimension" [ nospaceString $ show $ strictDimension t ]
-      ]
-     
-instance XmlContent Domain where
-   parseContents = error "parseContents not implemented"
-
-   toContents d = rmkel "domain" $ case d of
-       Naturals -> rmkel "naturals" []
-       Rationals delta -> rmkel "rationals" 
-         $ rmkel "delta" $ toContents delta
-       Arctic d -> rmkel "arctic" $ toContents d
-       Tropical d -> rmkel  "tropical" $ toContents d
-
-instance XmlContent Rational where
-    parseContents = error "parseContents not implemented"
-
-    toContents r = rmkel "rational" 
-        [ mkel "numerator"   [ nospaceString $ show $ numerator   r ]
-        , mkel "denominator" [ nospaceString $ show $ denominator r ]
-        ]
-
-instance XmlContent Interpret  where
-   parseContents = error "parseContents not implemented"
-
-   toContents i = rmkel "interpret" $ concat
-                    [ toContents $ symbol i
-                    , rmkel "arity" [ nospaceString $ show $ arity i ]
-                    , toContents $ value i
-                    ]
-
-instance XmlContent Value where
-   parseContents = error "parseContents not implemented"
-
-   toContents v = case v of
-      Polynomial p -> toContents p
-      ArithFunction f -> toContents f
-
-instance XmlContent Polynomial where
-   parseContents = error "parseContents not implemented"
-
-   toContents p = rmkel "polynomial" $ case p of
-       Sum     ps -> rmkel "sum"     $ concat ( map toContents ps )
-       Product ps -> rmkel "product" $ concat ( map toContents ps )
-       Polynomial_Coefficient c -> rmkel "coefficient" $ toContents c
-       Polynomial_Variable v -> rmkel "variable" [ nospaceString v ]
-
-instance XmlContent ArithFunction where
-  parseContents = error "parseContents not implemented"
-
-  toContents af = rmkel "arithFunction" $ case af of
-    AFNatural  n      -> rmkel "natural"  [ nospaceString $ show n ]
-    AFVariable n      -> rmkel "variable" [ nospaceString $ show n ]
-    AFSum     afs     -> rmkel "sum"      $ concatMap toContents afs
-    AFProduct afs     -> rmkel "product"  $ concatMap toContents afs
-    AFMin     afs     -> rmkel "min"      $ concatMap toContents afs
-    AFMax     afs     -> rmkel "max"      $ concatMap toContents afs
-    AFIfEqual a b t f -> rmkel "ifEqual"  $ concatMap toContents [a,b,t,f]
-
-instance XmlContent Coefficient where
-   parseContents = error "parseContents not implemented"
-
-   toContents v = case v of
-       Matrix vs -> rmkel "matrix" $ concat ( map toContents vs )
-       Vector cs -> rmkel "vector" $ concat ( map toContents cs )
-       Coefficient_Coefficient i -> 
-          rmkel "coefficient" $ toContents i
-
-instance XmlContent Exotic where
-    parseContents = error "parseContents not implemented"
-
-    toContents e = case e of
-       Minus_Infinite -> rmkel "minusInfinity" []
-       E_Integer i -> rmkel "integer" [ nospaceString $ show i ]
-       Plus_Infinite -> rmkel "plusInfinity" []
-
--- see remark in TPDB.Data.Xml (sharp_name_HACK)
-
-instance XmlContent Symbol where
-  parseContents = error "parseContents not implemented"
-
-  toContents (SymName id) = rmkel "name" [nospaceString $ show id]
-  toContents (SymSharp sym) = rmkel "sharp" $ toContents sym
-  toContents (SymLabel sym label) = rmkel "labeledSymbol" 
-                                  $ toContents sym ++ (toContents label)
-
-instance XmlContent Label where
-  parseContents = error "parseContents not implemented"
-
-  toContents (LblNumber is) = 
-    rmkel "numberLabel" $ map (\i -> mkel "number" [ nospaceString $ show i ]) is
-
-  toContents (LblSymbol ss) = rmkel "symbolLabel" $ concatMap toContents ss
-
-instance XmlContent PathOrder where
-  parseContents = error "parseContents not implemented"
-
-  toContents (PathOrder ps as) = rmkel "pathOrder" $ concat
-    [ rmkel "statusPrecedence" $ concatMap toContents ps
-    , if null as then []
-      else rmkel "argumentFilter" $ concatMap toContents as
-    ]
-
-instance XmlContent PrecedenceEntry where
-  parseContents = error "parseContents not implemented"
-
-  toContents (PrecedenceEntry s a p) = rmkel "statusPrecedenceEntry" $ concat
-    [ toContents s
-    , rmkel "arity"      [ nospaceString $ show a ]
-    , rmkel "precedence" [ nospaceString $ show p ]
-    , rmkel "lex"        [ ]
-    ]
-
-instance XmlContent ArgumentFilterEntry where
-  parseContents = error "parseContents not implemented"
-
-  toContents (ArgumentFilterEntry s a f) = rmkel "argumentFilterEntry" $ concat
-    [ toContents s
-    , rmkel "arity"      [ nospaceString $ show a ]
-    , case f of 
-        Left i   -> rmkel "collapsing" [ nospaceString $ show i ]
-        Right is -> rmkel "nonCollapsing" 
-                  $ map (\i -> mkel "position" [ nospaceString $ show i ]) is
-    ]
diff --git a/TPDB/CPF/Proof/Xml.hs b/TPDB/CPF/Proof/Xml.hs
deleted file mode 100644
--- a/TPDB/CPF/Proof/Xml.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-module TPDB.CPF.Proof.Xml 
-( module TPDB.CPF.Proof.Read
-, module TPDB.CPF.Proof.Write 
-) where
-import TPDB.CPF.Proof.Read
-import TPDB.CPF.Proof.Write 
diff --git a/TPDB/Convert.hs b/TPDB/Convert.hs
deleted file mode 100644
--- a/TPDB/Convert.hs
+++ /dev/null
@@ -1,41 +0,0 @@
-module TPDB.Convert where
-
-import TPDB.Data
-import Control.Monad ( forM, guard )
-
-srs2trs :: SRS Identifier -> TRS Identifier Identifier
-srs2trs s = s { separate = False
-              , rules = map convert_srs_rule $ rules s
-              }  
-
-convert_srs_rule u = 
-    let v = mk 0 "x"
-        set_arity a s = s { arity = a }
-        handle = unspine v . map (set_arity 1)
-    in  u { lhs = handle $ lhs u
-          , rhs = handle $ rhs u        
-          } 
-                  
-trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )
-trs2srs t = do
-    us <- forM ( rules t ) convert_trs_rule 
-    return $ t { separate = True , rules = us }
-
-convert_trs_rule u = do
-      ( left_spine, left_base ) <- spine $ lhs u
-      ( right_spine, right_base ) <- spine $ rhs u
-      guard $ left_base == right_base     
-      return $ u { lhs = left_spine, rhs = right_spine }
-
-unspine :: v -> [s] -> Term v s
-unspine v = foldr (  \ c t -> Node c [ t ] ) ( Var v )
-
--- | success iff term consists of unary symbols
--- and the lowest node is a variable
-spine :: Term v s -> Maybe ( [s], v )
-spine t = case t of
-    Node f args -> do
-      [ arg ] <- return args
-      ( sp, base ) <- spine arg 
-      return ( f : sp, base )
-    Var v -> return ( [] , v ) 
diff --git a/TPDB/DP.hs b/TPDB/DP.hs
deleted file mode 100644
--- a/TPDB/DP.hs
+++ /dev/null
@@ -1,7 +0,0 @@
-module TPDB.DP ( module TPDB.DP.Transform )
-
-where
-
-import TPDB.DP.Transform
-import TPDB.DP.Graph
-
diff --git a/TPDB/DP/Graph.hs b/TPDB/DP/Graph.hs
deleted file mode 100644
--- a/TPDB/DP/Graph.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-module TPDB.DP.Graph where
-
-import TPDB.DP.TCap
-import TPDB.DP.Unify
-import TPDB.DP.Transform 
-
-import TPDB.Data
-import TPDB.Pretty
-
-import TPDB.Plain.Read -- for testing
-import TPDB.Plain.Write -- for testing
-
-import qualified Data.Set as S
-import qualified Data.Map as M
-import Data.Graph ( stronglyConnComp, SCC(..) )
-import Control.Monad ( guard, forM )
-import Control.Applicative
-
-import Control.Monad.State.Strict 
-
-
--- | DP problems for strongly connected components, 
--- topologically sorted, with CyclicComponents in Right,
--- others in Left.
-components s = do 
-    let es = M.fromListWith (++) 
-           $ do (p,q) <- edges s ; return (p, [q])
-        key = M.fromList 
-            $ zip (filter strict $ rules s) [0.. ]
-    comp <- reverse $ stronglyConnComp $ do
-        p <- M.keys key
-        let qs = M.findWithDefault [] p es
-        return (p, key M.! p, map (key M.!) qs )
-    return $ case comp of
-        CyclicSCC vs -> Right $ s { rules = vs 
-                 ++ filter (not . strict) (rules s) } 
-        AcyclicSCC v -> Left v
-
--- | edges of the estimated dependency graph
-edges s = do
-    let def = S.filter isOriginal $ defined s
-    u <- filter strict $ rules s
-    v <- filter strict $ rules s
-    guard $ unifies ( vmap Left $ tcap s $ rhs u ) 
-                    ( vmap Right $ lhs v )
-    return (u,v)
-
-check = edges $ dp sys
-
--- example from "DP Revisited" http://colo6-c703.uibk.ac.at/ttt/rta04.pdf
-Right sys = 
-    TPDB.Plain.Read.trs "(VAR x y) (RULES not(not(x)) -> x not(or(x,y)) -> and(not(x),not(y)) not(and(x,y)) -> or (not(x),not(y)) and(x,or(y,z)) -> or(and(x,z),and(y,z)) and(or(y,z),x) -> or(and(x,y),and(x,z)))"
-
diff --git a/TPDB/DP/TCap.hs b/TPDB/DP/TCap.hs
deleted file mode 100644
--- a/TPDB/DP/TCap.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-module TPDB.DP.TCap where
-
-import TPDB.Data
-import TPDB.Pretty
-
-import TPDB.DP.Unify
-
-import Control.Monad.State.Strict 
-import Control.Applicative
-
-
--- |  This function keeps only those parts of the input term which cannot be reduced,
--- even if the term is instantiated. All other parts are replaced by fresh variables.
--- Def 4.4 in http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf
-
-tcap :: (Ord v, Ord c) => TRS v c -> Term v c -> Term Int c
-tcap dp t = evalState ( walk dp t ) 0
-
-fresh_var :: State Int ( Term Int c )
-fresh_var = do i <- get ; put $ succ i ; return $ Var i
-
-walk dp t = case t of
-    Node f args -> do
-        t' <- Node f <$> forM args (walk dp)
-        if all ( \ u -> not $ unifies ( vmap Left $ lhs u ) ( vmap Right t' ) )
-                   $ filter (not . strict) $ rules dp
-            then return t' else fresh_var
-    _ -> fresh_var 
-
diff --git a/TPDB/DP/Transform.hs b/TPDB/DP/Transform.hs
deleted file mode 100644
--- a/TPDB/DP/Transform.hs
+++ /dev/null
@@ -1,71 +0,0 @@
-{-# language OverloadedStrings #-}
-{-# LANGUAGE DeriveGeneric #-}
-
-module TPDB.DP.Transform  where
-
-import TPDB.Data
-import TPDB.Pretty
-
-import qualified Data.Set as S
-import Control.Monad ( guard, forM )
-
-import Data.Hashable
-import GHC.Generics
-
-data Marked a = Original a | Marked a | Auxiliary a
-    deriving ( Show, Eq, Ord, Generic )
-
-isOriginal m = case m of Original {} -> True ; _ -> False
-isMarked   m = case m of Marked   {} -> True ; _ -> False
-
-instance Hashable a => Hashable (Marked a) 
-
-instance Pretty a => Pretty ( Marked a) where
-   pretty m = case m of
-       Original a -> pretty a
-       Marked a -> pretty a <> "#"
-       Auxiliary a -> pretty a
-
-mark_top :: Term v a -> Term v (Marked a)
-mark_top  (Node f args) = 
-          Node (Marked f) $ map (fmap Original) args
-
-defined s = S.fromList $ do 
-                u <- rules s
-                let Node f args = lhs u
-                -- will raise exception if lhs is variable
-                return f
-
--- | compute the DP transformed system.
-
-dp :: (Ord v, Ord s) 
-   => RS s (Term v s) 
-   -> RS (Marked s) (Term v (Marked s))
-dp s = 
-   let os = map ( \ u -> Rule { relation = Weak
-                               , lhs = fmap Original $ lhs u  
-                               , rhs = fmap Original $ rhs u  
-                               , top = False
-                               } )
-           $ rules s
-       def = defined s
-       us = do 
-            u <- rules s
-            let ssubs = S.fromList $ strict_subterms $ lhs u
-                walk r = if S.member r ssubs then [] else case r of
-                    -- will raise exception if rhs contains 
-                    -- a variable that is not in lhs
-                    Node f args -> 
-                        ( if S.member f def then (r :) else id )
-                        ( args >>= walk )
-            r <- walk $ rhs u
-            return $ Rule { relation = Strict
-                          , lhs = mark_top $ lhs u
-                          , rhs = mark_top r 
-                          , top = True
-                          }
-   in RS { signature = map Marked ( S.toList def )
-                     ++ map Original ( signature s )
-         , rules = us ++ os
-         , separate = separate s 
-         } 
diff --git a/TPDB/DP/Unify.hs b/TPDB/DP/Unify.hs
deleted file mode 100644
--- a/TPDB/DP/Unify.hs
+++ /dev/null
@@ -1,57 +0,0 @@
-module TPDB.DP.Unify ( mgu, match, unifies, apply, times ) where
-
-import TPDB.Data
-import qualified Data.Map as M
-import Control.Monad ( guard, foldM )
-import Data.Maybe (isJust)
-
-type Substitution v c = M.Map v (Term v c)
-
-unifies t1 t2 = isJust $ mgu t1 t2
-
--- | view variables as symbols
-pack :: Term v c -> Term any (Either v c)
-pack ( Var v ) = Node ( Left v ) []
-pack ( Node f args ) = Node ( Right f ) ( map pack args )
-
-unpack :: Term any (Either v c) -> Term v c
-unpack ( Node ( Left v ) [] ) = Var v
-unpack ( Node ( Right f ) args ) = Node f ( map unpack args )
-
--- | will only bind variables in the left side
-match :: ( Ord v, Ord w, Eq c )
-      => Term v c
-      -> Term w c
-      -> Maybe ( M.Map v ( Term w c ) )
-match l r = do
-    u <- mgu ( fmap Right l ) ( pack r )
-    return $ M.map unpack  u
-
-
--- | naive implementation (worst case exponential)
-mgu
-  :: (Ord v, Eq c) =>
-     Term v c -> Term v c -> Maybe (M.Map v (Term v c))
-mgu t1 t2 | t1 == t2 = return M.empty
-mgu ( Var v ) t2 = do
-    guard $ not $ elem (Var v) $ subterms t2
-    return $ M.singleton v t2
-mgu t1 ( Var v ) = mgu ( Var v ) t1  
-mgu (Node f1 args1) (Node f2 args2) 
-    | f1 == f2 && length args1 == length args2 = do
-        guard $ f1 == f2
-        foldM ( \ s (l,r) -> do
-            t <- mgu (apply l s) (apply r s) 
-            return $ times s t ) M.empty $ zip args1 args2 
-mgu _ _ = Nothing
-   
-times :: Ord v 
-      => Substitution v c -> Substitution v c -> Substitution v c
-times s t = 
-    M.union ( M.difference t s )
-            ( M.map ( \ v -> apply v t ) s )
-
-apply t s = case t of
-    Var v -> case  M.lookup v s of Nothing -> t ; Just w -> w
-    Node f args -> Node f $ map (\ a -> apply a s) args
-    
diff --git a/TPDB/DP/Usable.hs b/TPDB/DP/Usable.hs
deleted file mode 100644
--- a/TPDB/DP/Usable.hs
+++ /dev/null
@@ -1,43 +0,0 @@
-module TPDB.DP.Usable where
-
-import TPDB.Data
-import TPDB.Pretty
-
-import TPDB.DP.Unify
-import TPDB.DP.TCap
-
-import qualified Data.Set as S
-
--- | DANGER: this ignores the CE condition
-restrict :: (Ord c, Ord v) => RS c (Term v c) -> RS c (Term v c)
-restrict dp = 
-    dp { rules = filter strict (rules dp)
-               ++ S.toList ( usable dp)
-       }
-
--- | computes the least closed set of usable rules, cf. Def 4.5
--- http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf
-
-usable ::   (Ord v, Ord c)
-       => TRS v c -> S.Set (Rule (Term v c))
-usable dp = fixpoint ( \ s -> S.union s $ required dp s)
-    (required dp $ S.filter strict
-                 $ S.fromList $ rules dp) 
-
-fixpoint f x = 
-    let y = f x in if x == y then x else fixpoint f y
-
-required ::  (Ord v, Ord c)
-       => TRS v c -> S.Set ( Rule (Term v c) ) ->  S.Set ( Rule (Term v c) ) 
-required dp rs = 
-    S.fromList $ do { r <- S.toList rs ;  needed dp $ rhs r }
-
-needed :: (Ord v, Ord c)
-       => TRS v c -> Term v c -> [ Rule (Term v c) ]
-needed dp t = case t of
-    Node f args -> 
-          filter ( \ u -> unifies ( vmap Left $ lhs u ) ( vmap Right $ tcap dp t ) )
-                ( filter (not . strict) $ rules dp )
-        ++ ( args >>= needed dp )
-    Var v -> []
-
diff --git a/TPDB/Data.hs b/TPDB/Data.hs
deleted file mode 100644
--- a/TPDB/Data.hs
+++ /dev/null
@@ -1,121 +0,0 @@
-{-# language DeriveDataTypeable #-}
-
-module TPDB.Data 
-
-( module TPDB.Data
-, module TPDB.Data.Term
-)
-
-where
-
-
-import TPDB.Data.Term
-
-import Data.Typeable
-import Control.Monad ( guard )
-
-import Data.Hashable
-import Data.Function (on)
-
-data Identifier = 
-     Identifier { _identifier_hash :: ! Int
-                , name :: ! String 
-                , arity :: Int 
-                }
-    deriving ( Eq, Ord, Typeable )
-
-instance Hashable Identifier where
-    hashWithSalt s i = hash (s, _identifier_hash i)
-
-instance Show Identifier where show = name
-
-mk :: Int -> String -> Identifier
-mk a n = Identifier { _identifier_hash = hash (a,n)
-                    , arity = a, name = n }
-
-
----------------------------------------------------------------------
-
-data Relation = Strict |  Weak | Equal deriving ( Eq, Ord, Typeable, Show )
-
-data Rule a = Rule { lhs :: a, rhs :: a 
-                   , relation :: Relation
-                   , top :: Bool
-                   }
-    deriving ( Eq, Ord, Typeable )
-
-strict :: Rule a -> Bool
-strict u = case relation u of Strict -> True ; _ -> False
-
-weak :: Rule a -> Bool
-weak u = case relation u of Weak -> True ; _ -> False
-
-equal :: Rule a -> Bool
-equal u = case relation u of Equal -> True ; _ -> False
-
-instance Functor (RS s) where
-    fmap f rs = rs { rules = map (fmap f) $ rules rs }
-
-instance Functor Rule where 
-    fmap f u = u { lhs = f $ lhs u, rhs = f $ rhs u } 
-
-data RS s r = 
-     RS { signature :: [ s ] -- ^ better keep order in signature (?)
-         , rules :: [ Rule r ]
-        , separate :: Bool -- ^ if True, write comma between rules
-         }
-   deriving ( Typeable )
-
-instance Eq r => Eq (RS s r) where
-    (==) = (==) `on` rules
-
-strict_rules sys = 
-    do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
-weak_rules sys = 
-    do u <- rules sys ; guard $ weak u ; return ( lhs u, rhs u )
-equal_rules sys = 
-    do u <- rules sys ; guard $ equal u ; return ( lhs u, rhs u )
-
-type TRS v s = RS s ( Term v s )
-
-type SRS s = RS s [ s ]
-
-data Problem v s = 
-     Problem { type_ :: Type 
-             , trs :: TRS v s
-             , strategy :: Maybe Strategy
-             -- , metainformation :: Metainformation
-             , startterm :: Maybe Startterm  
-             }
-
-data Type = Termination | Complexity
-     deriving Show 
-
-data Strategy = Full | Innermost | Outermost
-     deriving Show
-
-data Startterm = 
-       Startterm_Constructor_based
-       | Startterm_Full
-     deriving Show     
-
-------------------------------------------------------
-
--- | legaca stuff (used in matchbox)
-
-type TES = TRS Identifier Identifier
-type SES = SRS Identifier
-
-mknullary s = mk 0 s
-mkunary   s = mk 1 s
-
-from_strict_rules :: Bool -> [(t,t)] -> RS i t
-from_strict_rules sep rs = 
-    RS { rules = map ( \ (l,r) ->
-             Rule { relation = Strict, top = False, lhs = l, rhs = r } ) rs
-       , separate = sep 
-       }
-
-with_rules sys rs = sys { rules = rs }
-
-
diff --git a/TPDB/Data/Term.hs b/TPDB/Data/Term.hs
deleted file mode 100644
--- a/TPDB/Data/Term.hs
+++ /dev/null
@@ -1,166 +0,0 @@
-{-# language DeriveDataTypeable #-}
-
-module TPDB.Data.Term where
-
-import qualified Data.Set as S
-import Data.Set (Set)
-import Data.Typeable
-
-data Term v s = Var v 
-              | Node s [ Term v s ]
-    deriving ( Eq, Ord, Show, Typeable )
-
-vmap :: ( v -> u ) -> Term v s -> Term u s
-vmap f ( Var v ) = Var ( f v )
-vmap f ( Node c args ) = Node c $ map ( vmap f ) args
-
-instance Functor ( Term v ) where
-    fmap f ( Var v ) = Var v
-    fmap f ( Node c args ) = Node (f c) ( map ( fmap f ) args )
-
-
-
-type Position = [ Int ]
-
-positions :: Term v c 
-          -> [ ( Position, Term v c ) ]
-positions t = ( [], t ) : case t of
-    Node c args -> do ( k, arg ) <- zip [ 0 .. ] args
-		      ( p, s   ) <- positions arg
-		      return ( k : p , s )
-    _ -> []
-
--- | all positions
-pos :: Term v c 
-    -> [ Position ]
-pos t = do
-    ( p, s ) <- positions t
-    return p
-
--- | non-variable positions
-sympos :: Term v c 
-    -> [ Position ]
-sympos t = do
-    ( p, Node {} ) <- positions t
-    return p
-
--- | variable positions
-varpos :: Term v c 
-    -> [ Position ]
-varpos t = do
-    ( p, Var {} ) <- positions t
-    return p
-
--- | leaf positions (= nullary symbols)
-leafpos :: Term v c 
-    -> [ Position ]
-leafpos t = do
-    ( p, Node c [] ) <- positions t
-    return p
-
-
-{-# inline subterms #-}
-
-subterms :: Term v c 
-	 -> [ Term v c ]
-subterms t = t : case t of
-    Node c args -> do arg <- args
-		      subterms arg
-    _ -> []
-
--- Note: following implementation relies on @subterms@
--- returning the preorder list (where the full term goes first)
-strict_subterms t = tail $ subterms t
-
-isSubtermOf :: (Eq v, Eq c ) 
-         => Term v c ->  Term v c  -> Bool
-isSubtermOf s t = elem s $ subterms t
-
-isStrictSubtermOf :: (Eq v, Eq c ) 
-         => Term v c ->  Term v c  -> Bool
-isStrictSubtermOf s t = elem s $ strict_subterms t
-
--- | compute new symbol at position, giving the position
-pmap:: ( Position -> c -> d )
-     -> Term v c
-     -> Term v d
-pmap f = rpmap ( \ p c -> f ( reverse p) c )
-
--- | compute new symbol from *reverse* position and previous symbol
--- this is more efficient (no reverse needed)
-rpmap :: ( Position -> c -> d )
-     -> Term v c
-     -> Term v d
-rpmap f t = helper [] t where
-    helper p ( Node c args ) = Node ( f p c ) $ do
-	     ( k, arg ) <- zip [0..] args
-	     return $ helper ( k : p ) arg
-    helper p ( Var v) = Var v
-
-
-
-peek :: Term v c 
-     -> Position 
-     -> Term v c
-peek t [] = t
-peek ( Node c args ) ( k : ks ) = peek ( args !! k ) ks
-
-peek_symbol :: Term v c 
-     -> Position 
-     -> c
-peek_symbol t p = 
-    case peek t p of
-         Node c args -> c
-	 _ -> error "Autolib.TES.Position.peek_symbol called for non-symbol"
-
--- | warning: don't check arity
-poke_symbol ::  Term v c 
-     -> ( Position , c )
-     -> Term v c
-poke_symbol t ( p, c ) =  
-    case peek t p of
-         Node _ args -> poke t ( p, Node c args )
-	 _ -> error "Autolib.TES.Position.poke_symbol called for non-symbol"
-
-poke :: Term v c 
-     -> ( Position , Term v c )
-     -> Term v c
-poke t ( [], s ) = s
-poke (Node c args) (k : ks, s ) = 
-    let ( pre , this : post ) = splitAt k args
-    in Node c ( pre ++ poke this ( ks, s ) : post )
-
-pokes :: Term v c
-      -> [ ( Position, Term v c ) ]
-      -> Term v c
-pokes = foldl poke
-
-
--- | in preorder 
-symsl :: Term v c -> [ c ]
-symsl t = do
-    Node c _ <- subterms t
-    return c
-
-syms :: Ord c => Term v c -> Set c
-syms = S.fromList . symsl
-
-
-lsyms :: Ord c => Term v c -> [ c ]
-lsyms = S.toList . syms
-
-vars :: Ord v => Term v c -> Set v
-vars t = S.fromList $ do
-    Var v <- subterms t
-    return v
-
-isvar :: Term v c -> Bool
-isvar ( Var _ ) = True ; isvar _ = False
-
--- | list of variables (each occurs once, unspecified ordering)
-lvars :: Ord v => Term v c -> [ v ]
-lvars = S.toList . vars
-
--- | list of variables (in pre-order, with duplicates)
-voccs :: Term v c -> [ v ]
-voccs t = do ( p, Var v ) <- positions t ; return v
diff --git a/TPDB/Data/Xml.hs b/TPDB/Data/Xml.hs
deleted file mode 100644
--- a/TPDB/Data/Xml.hs
+++ /dev/null
@@ -1,81 +0,0 @@
-{-# language FlexibleContexts #-}
-{-# language FlexibleInstances #-}
-{-# language UndecidableInstances #-}
-
-module TPDB.Data.Xml where
-
-import TPDB.Data
-import TPDB.Xml
-
-import Text.XML.HaXml.Types (QName (..) )
-import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
-
-import Data.Typeable
-
--- | FIXME: move to separate module
-instance XmlContent Identifier where
-    parseContents = do
-        CString _ s _ <- next 
-        return  $ mknullary s
-    toContents i =
-          -- probably not here: E.xmlEscape E.stdXmlEscaper
-          -- this introduces whitespace between &lt; and =
-          -- [ CString False $ show i ]
-          -- and this creates a CDATA element
-          -- [ CString True $ show i ]
-          -- so here comes an UGLY HACK:
-          [ CString False ( escape $ show i ) () ]
-
-
-instance ( Typeable ( Term v c ) , XmlContent v, XmlContent c )
-         => XmlContent ( Term v c ) where
-    toContents ( Var v ) = rmkel "var" $ toContents v
-{-
--- for Rainbow:
-    toContents ( Node f xs ) = return $ mkel "app"
-         $ mkel "fun" ( toContents f )
-         : map ( \ x -> mkel "arg" $ toContents x ) xs
--}
--- for CPF:
-
--- the problem is this:
--- a variable is an Identifier, and must look like "<var>foo</var>"
--- a constructor symbol is also an Identifier
--- but it must look like "<funapp><name>bar<name>..."
--- so it should be wrapped into <name>
--- but no, if the constructor is sharped (or labelled)
--- then it must look like "<funapp><sharp><name>bar..."
--- price question: what is the correct 
--- instance XmlContent Identifier ?
--- the answer probably is "there is none",
--- and toContents (Term v Identifier) should never occur,
--- instead need to call  toContents (Term v Symbol)
-
-    toContents ( Node f args ) = rmkel "funapp" 
-            $ no_sharp_name_HACK ( toContents f )
-           ++ map ( \ arg -> mkel "arg" $ toContents arg ) args
-
-no_sharp_name_HACK e = e
-
-sharp_name_HACK e = case e of
-    [ CElem ( Elem (N "sharp") [] cs ) () ] -> 
-        rmkel "sharp" $ rmkel "name" cs
-    _ -> rmkel "name" e
-
-
-
-
-instance HTypeable ( Rule ( Term v c )) where
-     toHType _ = Prim "Rule" "Rule"
-
-instance ( HTypeable ( Rule ( Term v c) )
-         , XmlContent ( Term v c ) ) 
-         => XmlContent ( Rule ( Term v c ) ) where
-    toContents u =
-        return $ mkel "rule" 
-               [ mkel "lhs" $ toContents $ lhs u
-               , mkel "rhs" $ toContents $ rhs u
-               ]
-
-
-
diff --git a/TPDB/Input.hs b/TPDB/Input.hs
deleted file mode 100644
--- a/TPDB/Input.hs
+++ /dev/null
@@ -1,64 +0,0 @@
-module TPDB.Input where
-
-import TPDB.Data
-import TPDB.Plain.Read
-import TPDB.XTC.Read
-import TPDB.Convert
-
-import System.FilePath.Posix ( takeExtension )
-
--- | read input from file with given name.
--- can have extension .srs, .trs, .xml.
--- unknown extension is considered as .xml, because of 
--- http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks
-
-get :: FilePath 
-         -> IO ( Either (TRS Identifier Identifier) 
-                        ( SRS Identifier ) )
-get f = do
-    m <- getE f
-    case m of
-        Right x -> return x 
-        Left err -> error err
-
-getE f = case takeExtension f of
-      ".srs" -> do
-          s <- readFile f    
-          case srs s of
-              Left err -> return $ Left err
-              Right t -> return $ Right $ Right t
-      ".trs" -> do        
-          s <- readFile f
-          case TPDB.Plain.Read.trs s of
-              Left err -> return $ Left err
-              Right t -> return $ Right $ Left t 
-      _ -> do
-          ps <- readProblems f
-          case ps of 
-              [ p ] -> return $ Right $ Left $ TPDB.Data.trs p
-              [] -> return $ Left "no TRS"
-              _ -> return $ Left "more than one TRS"
-
-get_trs f = do
-    x <- get f
-    return $ case x of
-        Right x -> srs2trs x
-        Left  x -> x
-
-getE_trs f = do
-    e <- getE f
-    return $ case e of
-        Right x -> Right $ case x of
-            Right x -> srs2trs x
-            Left  x -> x
-        Left e -> Left e
-
-get_srs f = do
-    x <- get f
-    return $ case x of
-        Right x -> x
-        Left  x -> case trs2srs x of
-            Nothing -> error "not an SRS"
-            Just x -> x
-            
-
diff --git a/TPDB/Mirror.hs b/TPDB/Mirror.hs
deleted file mode 100644
--- a/TPDB/Mirror.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-module TPDB.Mirror where
-
-import TPDB.Data
-import TPDB.Convert
-
-import Control.Monad ( forM, guard )
-
--- | if input is SRS, reverse lhs and rhs of each rule
-mirror :: TRS Identifier s 
-       -> Maybe ( TRS Identifier s )
-mirror trs = do
-    us <- forM (rules trs) $ \ u -> do
-      ( left_spine, left_base ) <- spine $ lhs u
-      ( right_spine, right_base ) <- spine $ rhs u
-      guard $ left_base == right_base 
-      return $ u { lhs = unspine left_base $ reverse left_spine
-                 , rhs = unspine right_base $ reverse right_spine
-                 }
-    return $ trs { rules = us }
diff --git a/TPDB/Plain/Read.hs b/TPDB/Plain/Read.hs
deleted file mode 100644
--- a/TPDB/Plain/Read.hs
+++ /dev/null
@@ -1,146 +0,0 @@
--- | textual input,
--- cf. <http://www.lri.fr/~marche/tpdb/format.html>
-
-{-# language PatternSignatures, TypeSynonymInstances, FlexibleInstances #-}
-
-module TPDB.Plain.Read where
-
-import TPDB.Data
-
-import Text.Parsec
-import Text.Parsec.Token
-import Text.Parsec.Language
-import Text.Parsec.Char
-
-import TPDB.Pretty (pretty)
-import TPDB.Plain.Write ()
-
-import Control.Monad ( guard, void )
-import Data.List ( nub )
-
-trs :: String -> Either String ( TRS Identifier Identifier )
-trs s = case Text.Parsec.parse reader "input" s of
-    Left err -> Left $ show err
-    Right t  -> Right t
-
-srs :: String -> Either String ( SRS Identifier )
-srs s = case Text.Parsec.parse reader "input" s of
-    Left err -> Left $ show err
-    Right t  -> Right t
-
-type Parser = Parsec String () 
-
-class Reader a where reader :: Parser a
-
--- | warning: by definition, {}[] may appear in identifiers
-lexer = makeTokenParser
-    $ emptyDef
-       { identStart  = alphaNum <|> oneOf "_:!#$%&*+./<=>?@\\^|-~{}[]'"
-       , identLetter = alphaNum <|> oneOf "_:!#$%&*+./<=>?@\\^|-~{}[]'"
-       , commentLine = "" , commentStart = "" , commentEnd = ""
-       , reservedNames = [ "VAR", "THEORY", "STRATEGY", "RULES", "->", "->=" ]
-       }
-
-
-instance Reader Identifier where 
-    reader = do
-        i <- identifier lexer 
-	return $ mk 0 i
-
-instance Reader s =>  Reader [s] where
-    reader = many reader
-
--- NOTE: this is dangerous since we read the variables as constants,
--- and this needs to be patched up later.
--- NOTE: this is more dangerous as we do not set the arity of identifiers
-instance ( Reader v ) => Reader ( Term v Identifier ) where
-    reader = do
-        f  <- reader 
-        xs <- option [] $ parens lexer $ commaSep lexer reader
-        return $ Node ( f { arity = length xs } ) xs
-
-instance Reader u => Reader ( Rule u ) where
-    reader = do
-        l <- reader
-        rel <-  do reservedOp lexer "->"  ; return Strict
-          <|> do reservedOp lexer "->=" ; return Weak
-          -- FIXME: for the moment, we do not parse this
-          -- as it would deviate from published TPDB syntax
-          -- <|> do reservedOp lexer "=" ; return Equal
-        r <- reader
-        return $ Rule { lhs = l, relation = rel, top = False, rhs = r }
-
-data Declaration u
-     = Var_Declaration [ Identifier ]
-     | Theory_Declaration 
-     | Strategy_Declaration 
-     | Rules_Declaration [ Rule u ]
-     | Unknown_Declaration
-       -- ^ this is super-ugly: a parenthesized, possibly nested, 
-       -- possibly comma-separated, list of identifiers or strings
-
-declaration :: Reader u => Bool -> Parser ( Declaration u )
-declaration sep = parens lexer $ 
-           do reserved lexer "VAR" ; xs <- many reader 
-              return $ Var_Declaration xs
-       <|> do reserved lexer "THEORY" 
-              error "TPDB.Plain.Read: parser for THEORY decl. missing"
-       <|> do reserved lexer "STRATEGY" 
-              error "TPDB.Plain.Read: parser for THEORY decl. missing"
-       <|> do reserved lexer "RULES" 
-              us <- if sep then do 
-                        many $ do 
-                            u <- reader ; optional $ comma lexer
-                            return u
-                        -- yes, TPDB contains some trailing commas, e.g., z008
-                        -- ( RULES a b -> b a , )
-                    else many reader
-              return $ Rules_Declaration us
-       <|> do anylist ; return Unknown_Declaration
-
-anylist = void 
-        $ commaSep lexer 
-        $ many ( void ( identifier lexer ) <|> parens lexer anylist )
-
-instance Reader ( SRS Identifier ) where
-    reader = do 
-        many space
-        ds <- many $ declaration True
-	return $ make_srs ds
-
-instance Reader ( TRS Identifier Identifier ) where
-    reader = do
-        many space
-        ds <- many $ declaration False
-	return $ make_trs ds
-
-repair_signature_srs sys = 
-    let sig = nub $ do u <- rules sys ; lhs u ++ rhs u
-    in  sys { signature = sig }
-
-make_srs :: Eq s => [ Declaration [s] ] -> SRS s
-make_srs ds = repair_signature_srs $
-    let us = do Rules_Declaration us <- ds ; us        
-    in  RS { rules = us, separate = True }
-
-repair_signature_trs sys = 
-    let sig = nub $ do u <- rules sys ; lsyms ( lhs u ) ++ lsyms ( rhs u)
-    in  sys { signature = sig }
-
-make_trs :: [ Declaration ( Term Identifier Identifier ) ] 
-         -> TRS Identifier Identifier
-make_trs ds = repair_signature_trs $
-    let vs = do Var_Declaration vs <- ds ; vs
-        us = do Rules_Declaration us <- ds ; us
-        us' = repair_variables vs us
-    in  RS { rules = us', separate = False }
-
-
-repair_variables vars rules = do
-    let xform ( Node c [] ) | c `elem` vars = Var c
-	xform ( Node c args ) = Node c ( map xform args )
-    rule <- rules  
-    return $ rule { lhs = xform $ lhs rule
-		  , rhs = xform $ rhs rule
-		  }
-
diff --git a/TPDB/Plain/Write.hs b/TPDB/Plain/Write.hs
deleted file mode 100644
--- a/TPDB/Plain/Write.hs
+++ /dev/null
@@ -1,67 +0,0 @@
--- | the "old" TPDB format 
--- cf. <http://www.lri.fr/~marche/tpdb/format.html>
-
-{-# language FlexibleContexts #-}
-{-# language OverloadedStrings #-}
-
-module TPDB.Plain.Write where
-
-import TPDB.Data
-import TPDB.Pretty
-
-import Data.List ( nub )
-import Data.String ( fromString )
-
-instance Pretty Identifier where
-    pretty i = fromString $ name i
-
-instance ( Pretty v, Pretty s ) => Pretty ( Term v s ) where
-    pretty t = case t of
-        Var v -> pretty v
-        Node f xs -> case xs of
-            [] -> pretty f 
-            _  -> pretty f <+> parens ( fsep $ punctuate comma $ map pretty xs )
-
-instance PrettyTerm a => Pretty ( Rule a ) where
-    pretty u = hsep [ prettyTerm $ lhs u
-                    , case relation u of 
-                         Strict -> "->" 
-                         Weak -> "->="
-                         Equal -> "="
-                    -- FIXME: implement "top" annotation
-                    , prettyTerm $ rhs u
-                    ]
-
-class PrettyTerm a where 
-    prettyTerm :: a -> Doc
-
-instance Pretty s => PrettyTerm [s] where    
-    prettyTerm xs = hsep $ map pretty xs
-
-instance ( Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where
-    prettyTerm = pretty
-
-instance ( Pretty s, PrettyTerm r ) => Pretty ( RS s r ) where
-    pretty sys = vcat 
-        [ parens $ "RULES" <+>
-          vcat ( ( if separate sys then punctuate comma else id )
-                 $ map pretty $ rules sys 
-               )
-        -- FIXME: variables are not shown (and it is impossible to compute
-        -- them here, this is actually a TPDB format design error, 
-        -- since variables should be local (per rule), not global)
-        -- FIXME: output strategy, theory
-        ]
-
-instance ( Pretty s, Pretty r ) => Pretty ( Problem s r ) where
-    pretty p = vcat
-       [ pretty $ trs p 
-       , case strategy p of  
-             Nothing -> empty
-             Just s -> fsep [ "strategy"
-                            , fromString ( show s ) ]
-       , case startterm p of  
-             Nothing -> empty
-             Just s -> fsep [ "startterm"
-                            , fromString ( show s ) ] 
-       ]
diff --git a/TPDB/Pretty.hs b/TPDB/Pretty.hs
deleted file mode 100644
--- a/TPDB/Pretty.hs
+++ /dev/null
@@ -1,59 +0,0 @@
-module TPDB.Pretty 
-
-( Doc, SimpleDoc
-, render, renderCompact, displayIO
-, Pretty (..)
-, fsep , hsep, vsep, vcat, hcat
-, parens, brackets, angles, braces, enclose
-, punctuate, comma, nest
-, empty, text
-, (<>), (<+>), ($$)
-)
-
-where
-
-import Text.PrettyPrint.Leijen.Text 
-    hiding ( text, (<+>), vcat )
-import qualified Text.PrettyPrint.Leijen.Text 
-import Data.String ( fromString )
-
--- class Pretty a where pretty :: a -> Doc
-
-fsep = fillSep
-($$) = (<$$>)
-x <+> y = x Text.PrettyPrint.Leijen.Text.<+> align y
-vcat = align . Text.PrettyPrint.Leijen.Text.vcat
-
-render :: Doc -> String
-render = show
-
-text :: String -> Doc
-text = fromString
-
-{-
-
-instance Pretty Int where pretty = text . show
-
-instance ( Pretty a, Pretty b ) => Pretty (a,b) where
-    pretty (x,y) = parens $ fsep $ punctuate comma [ pretty x, pretty y ]
-
-instance ( Pretty a, Pretty b, Pretty c ) => Pretty (a,b,c) where
-    pretty (x,y,z) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z ]
--}
-
-instance ( Pretty a, Pretty b, Pretty c, Pretty d ) => Pretty (a,b,c,d) where
-    pretty (x,y,z,u) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z, pretty u ]
-
-{-
-instance Pretty a => Pretty [a]  where
-    pretty xs = brackets $ fsep $ punctuate comma $ map pretty xs
-
-instance Pretty a => Pretty (Maybe a) where
-    pretty m = case m of
-        Nothing -> text "Nothing"
-        Just x -> text "Just" <+> pretty x -- FIXME: parens missing
--}
-
-instance ( Pretty a, Pretty b ) => Pretty (Either a b) where
-    pretty (Left x) = text "Left" <+> parens (pretty x)
-    pretty (Right x) = text "Right" <+> parens (pretty x)
diff --git a/TPDB/XTC.hs b/TPDB/XTC.hs
deleted file mode 100644
--- a/TPDB/XTC.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-module TPDB.XTC 
-
-( module TPDB.Data
-, module TPDB.XTC.Read
-)
-
-
-where
-
-import TPDB.Data
-import TPDB.XTC.Read
-
diff --git a/TPDB/XTC/Read.hs b/TPDB/XTC/Read.hs
deleted file mode 100644
--- a/TPDB/XTC/Read.hs
+++ /dev/null
@@ -1,109 +0,0 @@
-{-# language Arrows, NoMonomorphismRestriction, PatternSignatures #-}
-
--- | construct data object from XML tree.
-
-module TPDB.XTC.Read where
-
--- implementations follows these examples:
--- http://www.haskell.org/haskellwiki/HXT/Practical/
-
-import TPDB.Data
-
-import Text.XML.HXT.Arrow.XmlArrow
-
-import Text.XML.HXT.Arrow.XmlState ( runX )
-import Text.XML.HXT.Arrow.ReadDocument ( readString )
-import Text.XML.HXT.Arrow.XmlOptions ( a_validate )
-import Text.XML.HXT.DOM.XmlKeywords (v_0)
-import Control.Arrow
-import Control.Arrow.ArrowList
-import Control.Arrow.ArrowTree
-
-atTag tag = deep (isElem >>> hasName tag)
-
-getTerm = getVar <+> getFunApp
-
-getVar = proc x -> do
-    nm <- getText <<< getChildren <<< hasName "var" -< x
-    returnA -< Var $ mk 0 nm
-
-getFunApp = proc x -> do
-    sub <- hasName "funapp" -< x
-    nm <- getText <<< gotoChild "name" -< sub
-    gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub
-    let c = mk (length gs) nm
-    returnA -< Node c gs
-          
-gotoChild tag = proc x -> do
-    returnA <<< getChildren <<< getChild tag -< x
-
-getChild tag = proc x -> do
-    returnA <<< hasName tag <<< isElem <<< getChildren -< x
-
-getProblem = atTag "problem" >>> proc x -> do
-    ty <- getType <<< getAttrValue "type" -< x
-    rs <- getTRS <<< getChild "trs" -< x
-    st <- getStrategy <<< getChild "strategy" -< x
-    stt <- listA ( getStartterm <<< getChild "startterm" ) -< x
-    returnA -< Problem { trs = rs
-                        , TPDB.Data.strategy = st
-                        , type_ = ty 
-                        , startterm = case stt of
-                             [] -> Nothing
-                             [x] -> x
-                        }
-
-getType = proc x -> do
-    returnA -< case x of
-        "termination" -> Termination
-        "complexity" -> Complexity
-
-getStrategy = proc x -> do
-    cs <- getText <<< getChildren -< x
-    returnA -< case cs of
-        "FULL" -> Just Full
-
-getStartterm = ( proc x -> do
-        getChild "constructor-based" -< x
-        returnA -< Just Startterm_Constructor_based
-   ) <+>  ( proc x -> do
-        getChild "full" -< x
-        returnA -< Just Startterm_Full
-   ) <+> ( proc x -> do returnA -< Nothing )
-
-getTRS = proc x -> do
-    sig <- getSignature <<< getChild "signature" -< x
-    str <- getRules Strict <<< getChild "rules" -< x
-    nostr <- listA ( getRules Weak <<< getChild "relrules" <<< getChild "rules" ) -< x
-    -- FIXME: check that symbols are use with correct arity
-    th <- listA ( atTag "theory" ) -< x
-    returnA -< case th of
-        [] -> RS { signature = sig
-                  , rules = str ++ concat nostr
-                  , separate = False -- for TRS, don't need comma between rules
-                  }
-        _  -> error $ unwords [ "cannot handle theories" ]
-
-getSignature = proc x -> do
-    returnA <<< listA ( getFuncsym <<< getChild "funcsym" ) -< x
-
-getFuncsym = proc x -> do
-    nm <- getText <<< gotoChild "name" -< x
-    ar <- getText <<< gotoChild "arity" -< x
-    returnA -< mk (read ar) nm
-
-getRules str = proc x -> do
-    returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x
-
-getRule str = proc x -> do
-    l <-  getTerm <<< isElem <<< gotoChild "lhs" -< x
-    r <-  getTerm <<< isElem <<< gotoChild "rhs" -< x
-    returnA -< Rule { lhs = l, relation = str, rhs = r, top = False }
-
-readProblems :: FilePath -> IO [ Problem Identifier Identifier ]
-readProblems file = do
-    cs <- readFile file
-    runX ( readString [] cs >>> getProblem )
-
-
-
diff --git a/TPDB/Xml.hs b/TPDB/Xml.hs
deleted file mode 100644
--- a/TPDB/Xml.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-{-# language UndecidableInstances, OverlappingInstances, IncoherentInstances, FlexibleInstances, ScopedTypeVariables #-}
-
-module TPDB.Xml where
-
-import Text.XML.HaXml.Types (QName (..) )
-import Text.XML.HaXml.XmlContent.Haskell
-import Text.XML.HaXml.Posn ( Posn )
-
-import qualified Text.XML.HaXml.Pretty as P
-
-import Data.Typeable
-
-mkel name cs = CElem ( Elem (N name) [] cs ) ()
-rmkel name cs = return $ mkel name cs
-
-nospaceString :: String -> Content ()
-nospaceString s = CString False (escape s) ()
-
-instance Typeable t => HTypeable t where 
-    toHType x = let cs = show ( typeOf x ) in Prim cs cs
-
-escape [] = []
-escape ( c : cs ) = case c of
-    '<' -> "&lt;" ++ escape cs
-    '>' -> "&gt;" ++ escape cs
-    _   -> c :       escape cs
-
-
-type Contents = [ Content Posn ]
-
-data CParser a = CParser { unCParser :: Contents -> Maybe ( a, Contents ) }
-
-instance Functor CParser where
-    fmap f (CParser p) = CParser $ \ cs ->
-        do ( x, cs' ) <- p cs ; return ( f x, cs' )
-
-instance Monad CParser where
-    return x = CParser $ \ cs -> return ( x, cs )
-    CParser p >>= f = CParser $ \ cs0 -> 
-        do ( x, cs1 ) <- p cs0 ; unCParser ( must_succeed $ f x ) cs1
-
-
-must_succeed :: CParser a -> CParser a
-must_succeed (CParser p ) = CParser $ \ cs -> 
-    case p cs of
-        Nothing -> error $ "must succeed:" ++ errmsg cs
-	ok -> ok
-
-class Typeable a => XRead a where xread :: CParser a
-
-
-instance ( Typeable a, XmlContent a ) => XRead a where
-    xread = CParser $ \ cs -> case runParser parseContents cs of
-          ( Right x, rest ) -> Just ( x, rest )  
-          ( Left err, rest ) -> Nothing
-
-wrap :: forall a . Typeable a => CParser a -> Parser ( Content Posn ) a
-wrap ( CParser p ) = P $ \ cs -> case p cs of
-     Nothing -> Failure cs $ unlines
-	     $ "want expression of type " 
-	     :  show ( typeOf ( undefined :: a )) 
-	     :  errmsg cs
-	     : []
-     Just ( x, cs' ) -> Committed ( Success cs' x )
-
-errmsg cs = unlines $ case cs of 
-		  ( c  : etc ) -> 
-		     [ show $ P.content c
-		    
-		     ]
-		  _ -> [ show $ length cs ]
-
-orelse :: CParser a -> CParser a  -> CParser a
-orelse ( CParser p ) ( CParser q ) = CParser $ \ cs -> 
-    case p cs of Nothing -> q cs ; ok -> ok
-
-many :: CParser a -> CParser [a]
-many p = ( do x <- p ; xs <- TPDB.Xml.many p ; return $ x : xs ) `orelse` return []
-
-element tag p = element0 (N tag) $ must_succeed p
-
-element0 tag p = CParser $ \ cs -> case strip cs of
-     ( CElem ( Elem name atts con ) _ : etc ) | name == tag -> 
-         case unCParser p con of
-	     Nothing -> Nothing
-	     Just ( x, _ ) -> Just ( x, etc )
-     _ -> Nothing
-
-strip [] = []
-strip input @ ( CElem ( Elem {} ) _ : _ ) = input
-strip (c : cs) = strip cs
-
-xfromstring :: Read a => CParser a
-xfromstring = CParser $ \ cs -> case cs of
-    ( CString _ s _ : etc ) -> Just ( read s, etc )
-    _ -> Nothing
-
-complain :: String -> CParser a
-complain tag = CParser $ \ cs -> error $ "ERROR: in branch for " ++ tag ++ errmsg cs
-
-info :: Contents -> String
-info [] = "empty contents"
-info ( c : cs ) = case c of
-    CElem ( Elem name atts con ) _ -> "CElem, name: " ++ show name
-    CString _ s _ -> "CString : " ++ s
-    CRef _ _ -> "CRef"
-    CMisc _ _ -> "CMisc"
-
-
-
diff --git a/TPDB/Xml/Pretty.hs b/TPDB/Xml/Pretty.hs
deleted file mode 100644
--- a/TPDB/Xml/Pretty.hs
+++ /dev/null
@@ -1,298 +0,0 @@
--- | original author: Malcolm Wallace, 
--- license: LGPL
--- http://hackage.haskell.org/packages/archive/HaXml/1.23.3/doc/html/Text-XML-HaXml-Pretty.html
---
--- modified by Johannes Waldmann
--- to use a different pretty-printer back-end.
---
--- This is a pretty-printer for turning the internal representation
---   of generic structured XML documents into the Doc type (which can
---   later be rendered using Text.PrettyPrint.HughesPJ.render).
---   Essentially there is one pp function for each type in
---   Text.Xml.HaXml.Types, so you can pretty-print as much or as little
---   of the document as you wish.
-
-{-# language OverloadedStrings #-}
-
-module TPDB.Xml.Pretty
-  (
-  -- * Pretty-print a whole document
-    document
-  -- ** Just one content
-  ,   content
-  -- ** Just one tagged element
-  ,   element
-  -- * Pretty-print just a DTD
-  , doctypedecl
-  -- ** The prolog
-  ,   prolog
-  -- ** A content particle description
-  ,   cp
-  ) where
-
-import Prelude hiding (maybe,either)
-import Data.Maybe hiding (maybe)
-import Data.List (intersperse)
---import Char (isSpace)
-
--- import Text.PrettyPrint.HughesPJ
-import TPDB.Pretty hiding ( text )
-
-import Text.XML.HaXml.Types
-import Text.XML.HaXml.Namespaces
-
-import Data.String ( fromString )
-
-text = fromString
-
-either :: (t -> t1) -> (t2 -> t1) -> Either t t2 -> t1
-either f _ (Left x)  = f x
-either _ g (Right x) = g x
-
-maybe :: (t -> Doc) -> Maybe t -> Doc
-maybe _ Nothing  = empty
-maybe f (Just x) = f x
-
---peref p   = "%" <> text p <> ";"
-
-----
-
-document :: Document i -> Doc
-prolog   :: Prolog -> Doc
-xmldecl  :: XMLDecl -> Doc
-misc     :: Misc -> Doc
-sddecl   :: Bool -> Doc
-
-doctypedecl :: DocTypeDecl -> Doc
-markupdecl  :: MarkupDecl -> Doc
---extsubset   :: ExtSubset -> Doc
---extsubsetdecl :: ExtSubsetDecl -> Doc
-cp          :: CP -> Doc
-
-element   :: Element i -> Doc
-attribute :: Attribute -> Doc                     --etc
-content   :: Content i -> Doc
-
-----
-
-document (Document p _ e m)= prolog p $$ element e $$ vcat (map misc m)
-prolog (Prolog x m1 dtd m2)= maybe xmldecl x $$
-                             vcat (map misc m1) $$
-                             maybe doctypedecl dtd $$
-                             vcat (map misc m2)
-xmldecl (XMLDecl v e sd)   = "<?xml version='" <> text v <> "'" <+>
-                             maybe encodingdecl e <+>
-                             maybe sddecl sd <+>
-                             "?>"
-misc (Comment s)           = "<!--" <> text s <> "-->"
-misc (PI (n,s))            = "<?" <> text n <+> text s <> "?>"
-sddecl sd   | sd           = "standalone='yes'"
-            | otherwise    = "standalone='no'"
-doctypedecl (DTD n eid ds) = if null ds then
-                                  hd <> ">"
-                             else hd <+> " [" $$
-                                  vcat (map markupdecl ds) $$ "]>"
-                           where hd = "<!DOCTYPE" <+> qname n <+>
-                                      maybe externalid eid
-markupdecl (Element e)     = elementdecl e
-markupdecl (AttList a)     = attlistdecl a
-markupdecl (Entity e)      = entitydecl e
-markupdecl (Notation n)    = notationdecl n
-markupdecl (MarkupMisc m)  = misc m
---markupdecl (MarkupPE p m)  = peref p
-
---extsubset (ExtSubset t ds) = maybe textdecl t $$
---                             vcat (map extsubsetdecl ds)
---extmarkupdecl (ExtMarkupDecl m)      = markupdecl m
---extsubsetdecl (ExtConditionalSect c) = conditionalsect c
--- -- extsubsetdecl (ExtPEReference p e)   = peref p
-
-element (Elem n as []) = "<" <> qname n <+>
-                         fsep (map attribute as) <> "/>"
-element e@(Elem n as cs)
-    | all isText cs    = "<" <> qname n <+> fsep (map attribute as) <>
-                         ">" <> hcat (map content cs) <>
-                         "</" <> qname n <> ">"
-    | otherwise        = let (d,c) = carryelem e empty
-                         in d <> c
-
-isText :: Content t -> Bool
-isText (CString _ _ _) = True
-isText (CRef _ _)      = True
-isText _               = False
-
-carryelem    ::  Element t  -> Doc -> (Doc, Doc)
-carrycontent ::  Content t  -> Doc -> (Doc, Doc)
-spancontent  :: [Content a] -> Doc -> ([Doc],Doc)
-
-carryelem (Elem n as []) c = ( c <>
-                               "<" <> qname n <+> fsep (map attribute as)
-                             , "/>")
-carryelem (Elem n as cs) c =  let (cs0,d0) = spancontent cs (">") in
-                              ( c <>
-                                "<"<>qname n <+> fsep (map attribute as) $$
-                                nest 2 (vcat cs0) <>
-                                d0 <> "</" <> qname n
-                              , ">")
-
-carrycontent (CElem e _) c         = carryelem e c
-carrycontent (CString False s _) c = (c <> chardata s, empty)
-carrycontent (CString True  s _) c = (c <> cdsect s, empty)
-carrycontent (CRef r _) c          = (c <> reference r, empty)
-carrycontent (CMisc m _) c         = (c <> misc m, empty)
-
-spancontent []     c = ([],c)
-spancontent (a:as) c | isText a  = let (ts,rest) = span isText (a:as)
-                                       formatted = c <> hcat (map content ts)
-                                   in  spancontent rest formatted
-                     | otherwise = let (b, c0) = carrycontent a c
-                                       (bs,c1) = spancontent as c0
-                                   in  (b:bs, c1)
-
-attribute (n,v)             = qname n <> "=" <> attvalue v
-content (CElem e _)         = element e
-content (CString False s _) = chardata s
-content (CString True s _)  = cdsect s
-content (CRef r _)          = reference r
-content (CMisc m _)         = misc m
-
-elementdecl :: ElementDecl -> Doc
-elementdecl (ElementDecl n cs) = "<!ELEMENT" <+> qname n <+>
-                                 contentspec cs <> ">"
-contentspec :: ContentSpec -> Doc
-contentspec EMPTY              = "EMPTY"
-contentspec ANY                = "ANY"
-contentspec (Mixed m)          = mixed m
-contentspec (ContentSpec c)    = cp c
---contentspec (ContentPE p cs)   = peref p
-cp (TagName n m)       = parens (qname n) <> modifier m
-cp (Choice cs m)       = parens (hcat (intersperse ("|") (map cp cs))) <>
-                           modifier m
-cp (Seq cs m)          = parens (hcat (intersperse (",") (map cp cs))) <>
-                           modifier m
---cp (CPPE p c)          = peref p
-modifier :: Modifier -> Doc
-modifier None          = empty
-modifier Query         = "?"
-modifier Star          = "*"
-modifier Plus          = "+"
-mixed :: Mixed -> Doc
-mixed  PCDATA          = "(#PCDATA)"
-mixed (PCDATAplus ns)  = "(#PCDATA |" <+>
-                         hcat (intersperse ("|") (map qname ns)) <>
-                         ")*"
-
-attlistdecl :: AttListDecl -> Doc
-attlistdecl (AttListDecl n ds) = "<!ATTLIST" <+> qname n <+>
-                                 fsep (map attdef ds) <> ">"
-attdef :: AttDef -> Doc
-attdef (AttDef n t d)          = qname n <+> atttype t <+> defaultdecl d
-atttype :: AttType -> Doc
-atttype  StringType            = "CDATA"
-atttype (TokenizedType t)      = tokenizedtype t
-atttype (EnumeratedType t)     = enumeratedtype t
-tokenizedtype :: TokenizedType -> Doc
-tokenizedtype ID               = "ID"
-tokenizedtype IDREF            = "IDREF"
-tokenizedtype IDREFS           = "IDREFS"
-tokenizedtype ENTITY           = "ENTITY"
-tokenizedtype ENTITIES         = "ENTITIES"
-tokenizedtype NMTOKEN          = "NMTOKEN"
-tokenizedtype NMTOKENS         = "NMTOKENS"
-enumeratedtype :: EnumeratedType -> Doc
-enumeratedtype (NotationType n)= notationtype n
-enumeratedtype (Enumeration e) = enumeration e
-notationtype :: [String] -> Doc
-notationtype ns                = "NOTATION" <+>
-                                 parens (hcat (intersperse ("|") (map text ns)))
-enumeration :: [String] -> Doc
-enumeration ns                 = parens (hcat (intersperse ("|") (map nmtoken ns)))
-defaultdecl :: DefaultDecl -> Doc
-defaultdecl  REQUIRED          = "#REQUIRED"
-defaultdecl  IMPLIED           = "#IMPLIED"
-defaultdecl (DefaultTo a f)    = maybe (const ("#FIXED")) f <+> attvalue a
---conditionalsect (IncludeSect i)= "<![INCLUDE [" <+>
---                                 vcat (map extsubsetdecl i) <+> "]]>"
---conditionalsect (IgnoreSect i) = "<![IGNORE [" <+>
---                                 fsep (map ignoresectcontents i) <+> "]]>"
---ignore (Ignore)                = empty
---ignoresectcontents (IgnoreSectContents i is)
---                               = ignore i <+> vcat (map internal is)
---                          where internal (ics,i) = "<![[" <+>
---                                                   ignoresectcontents ics <+>
---                                                   "]]>" <+> ignore i
-reference :: Reference -> Doc
-reference (RefEntity er)       = entityref er
-reference (RefChar cr)         = charref cr
-entityref :: String -> Doc
-entityref n                    = "&" <> text n <> ";"
-charref :: (Show a) => a -> Doc
-charref c                      = "&#" <> text (show c) <> ";"
-entitydecl :: EntityDecl -> Doc
-entitydecl (EntityGEDecl d)    = gedecl d
-entitydecl (EntityPEDecl d)    = pedecl d
-gedecl :: GEDecl -> Doc
-gedecl (GEDecl n ed)           = "<!ENTITY" <+> text n <+> entitydef ed <>
-                                 ">"
-pedecl :: PEDecl -> Doc
-pedecl (PEDecl n pd)           = "<!ENTITY %" <+> text n <+> pedef pd <>
-                                 ">"
-entitydef :: EntityDef -> Doc
-entitydef (DefEntityValue ew)  = entityvalue ew
-entitydef (DefExternalID i nd) = externalid i <+> maybe ndatadecl nd
-pedef :: PEDef -> Doc
-pedef (PEDefEntityValue ew)    = entityvalue ew
-pedef (PEDefExternalID eid)    = externalid eid
-externalid :: ExternalID -> Doc
-externalid (SYSTEM sl)         = "SYSTEM" <+> systemliteral sl
-externalid (PUBLIC i sl)       = "PUBLIC" <+> pubidliteral i <+>
-                                 systemliteral sl
-ndatadecl :: NDataDecl -> Doc
-ndatadecl (NDATA n)            = "NDATA" <+> text n
---textdecl (TextDecl vi ed)      = "<?xml" <+> maybe text vi <+>
---                                 encodingdecl ed <+> "?>"
---extparsedent (ExtParsedEnt t c)= maybe textdecl t <+> content c
---extpe (ExtPE t esd)            = maybe textdecl t <+>
---                                 vcat (map extsubsetdecl esd)
-notationdecl :: NotationDecl -> Doc
-notationdecl (NOTATION n e)    = "<!NOTATION" <+> text n <+>
-                                 either externalid publicid e <>
-                                 ">"
-publicid :: PublicID -> Doc
-publicid (PUBLICID p)          = "PUBLIC" <+> pubidliteral p
-encodingdecl :: EncodingDecl -> Doc
-encodingdecl (EncodingDecl s)  = "encoding='" <> text s <> "'"
-nmtoken :: String -> Doc
-nmtoken s                      = text s
-attvalue :: AttValue -> Doc
-attvalue (AttValue esr)        = "\"" <>
-                                 hcat (map (either text reference) esr) <>
-                                 "\""
-entityvalue :: EntityValue -> Doc
-entityvalue (EntityValue evs)
-  | containsDoubleQuote evs    = "'"  <> hcat (map ev evs) <> "'"
-  | otherwise                  = "\"" <> hcat (map ev evs) <> "\""
-ev :: EV -> Doc
-ev (EVString s)                = text s
---ev (EVPERef p e)               = peref p
-ev (EVRef r)                   = reference r
-pubidliteral :: PubidLiteral -> Doc
-pubidliteral (PubidLiteral s)
-    | '"' `elem` s             = "'" <> text s <> "'"
-    | otherwise                = "\"" <> text s <> "\""
-systemliteral :: SystemLiteral -> Doc
-systemliteral (SystemLiteral s)
-    | '"' `elem` s             = "'" <> text s <> "'"
-    | otherwise                = "\"" <> text s <> "\""
-chardata :: String -> Doc
-chardata s                     = {-if all isSpace s then empty else-} text s
-cdsect :: String -> Doc
-cdsect c                       = "<![CDATA[" <> chardata c <> "]]>"
-
-qname n                        = text (printableName n)
-
-----
-containsDoubleQuote :: [EV] -> Bool
-containsDoubleQuote evs = any csq evs
-    where csq (EVString s) = '"' `elem` s
-          csq _            = False
diff --git a/src/TPDB/CPF/Proof/Read.hs b/src/TPDB/CPF/Proof/Read.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/CPF/Proof/Read.hs
@@ -0,0 +1,117 @@
+{-# language Arrows, NoMonomorphismRestriction, PatternSignatures #-}
+
+module TPDB.CPF.Proof.Read where
+
+import TPDB.CPF.Proof.Type 
+import TPDB.Data
+
+import Text.XML.HXT.Arrow.XmlArrow
+
+import Text.XML.HXT.Arrow.XmlState ( runX )
+import Text.XML.HXT.Arrow.ReadDocument ( readString )
+import Text.XML.HXT.Arrow.XmlOptions ( a_validate )
+import Text.XML.HXT.DOM.XmlKeywords (v_0)
+import Control.Arrow
+import Control.Arrow.ArrowList
+import Control.Arrow.ArrowTree
+
+import qualified TPDB.CPF.Proof.Write as W -- for testing
+import qualified Text.XML.HXT.Arrow.XmlState as X 
+
+{- | dangerous: 
+not all constructor arguments will be set.
+the function produces something like
+
+      CertificationProblem { input = CertificationProblemInput 
+                          , proof = TrsTerminationProof undefined
+                          }  
+-}
+
+readCP :: String -> IO [ CertificationProblem ]
+readCP = readCP_with_tracelevel 0
+
+readCP_with_tracelevel l s = runX ( X.withTraceLevel l $ readString [] s >>> getCP )
+
+getCP = getChild "certificationProblem" >>> proc x -> do
+    inp <- getInput <<< getChild "input" -< x
+    pro <- getProof <<< getChild "proof" -< x
+    ver <- getText <<< gotoChild "cpfVersion" -< x
+    returnA -< CertificationProblem 
+        { input = inp, proof = pro, cpfVersion = ver, origin = ignoredOrigin }
+
+getInput = getTerminationInput <+> getComplexityInput
+
+getTerminationInput = hasName "input" >>> proc x -> do
+    trsI <- getTrsInput <<< getChild "trsInput" -< x    
+    returnA -< TrsInput $ RS { rules = trsI, separate = False }
+
+getComplexityInput = hasName "input" >>> proc x -> do
+    y <- getChild "complexityInput" -< x
+    trsI <- getTrsInput <<< getChild "trsInput" -< y
+    cm <- getComplexityMeasure -< y
+    cc <- getComplexityClass -< y
+    returnA -< ComplexityInput
+        { trsinput_trs = RS { rules = trsI, separate = False }
+        , complexityMeasure = cm
+        , complexityClass = cc
+        }
+
+getComplexityMeasure = 
+        getDummy "derivationalComplexity" DerivationalComplexity
+    <+> getDummy "runtimeComplexity" RuntimeComplexity
+
+getComplexityClass = proc x -> do
+    d <- getText <<< gotoChild "polynomial" -< x
+    returnA -< ComplexityClassPolynomial { degree = read d }
+
+getTrsInput = proc x -> do
+    sys <- getTrs <<< getChild "trs" -< x
+    rels <- listA ( getTrsWith Weak <<< getChild "relativeRules" ) -< x
+    returnA -< sys ++ concat rels
+
+getTrs = getTrsWith Strict
+
+getTrsWith s = proc x -> do
+    str <- getRules s <<< getChild "rules" -< x
+    returnA -< str
+
+getProof = getDummy "trsTerminationProof" ( TrsTerminationProof undefined )
+       <+> getDummy "trsNonterminationProof" ( TrsNonterminationProof undefined )
+       <+> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined )
+       <+> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined )
+       <+> getDummy "complexityProof" ( ComplexityProof undefined )
+
+getDummy t c = proc x -> do 
+    getChild t -< x
+    returnA -< c 
+
+getRules str = proc x -> do
+    returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x
+
+getRule str = proc x -> do
+    l <-  getTerm <<< isElem <<< gotoChild "lhs" -< x
+    r <-  getTerm <<< isElem <<< gotoChild "rhs" -< x
+    returnA -< Rule { lhs = l, relation = str, rhs = r, top = False }
+
+
+getTerm = getVar <+> getFunApp
+
+getVar = proc x -> do
+    nm <- getText <<< getChildren <<< hasName "var" -< x
+    returnA -< Var $ mk 0 nm
+
+getFunApp = proc x -> do
+    sub <- hasName "funapp" -< x
+    nm <- getText <<< gotoChild "name" -< sub
+    gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub
+    let c = mk (length gs) nm
+    returnA -< Node c gs
+          
+gotoChild tag = proc x -> do
+    returnA <<< getChildren <<< getChild tag -< x
+
+getChild tag = proc x -> do
+    returnA <<< hasName tag <<< isElem <<< getChildren -< x
+
+
+
diff --git a/src/TPDB/CPF/Proof/Type.hs b/src/TPDB/CPF/Proof/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/CPF/Proof/Type.hs
@@ -0,0 +1,215 @@
+{-# language StandaloneDeriving #-}
+{-# language ExistentialQuantification #-}
+{-# language DeriveDataTypeable #-}
+
+-- | internal representation of CPF termination proofs,
+-- see <http://cl-informatik.uibk.ac.at/software/cpf/>
+
+module TPDB.CPF.Proof.Type 
+
+( module TPDB.CPF.Proof.Type
+, Identifier
+, TES
+)
+
+where
+
+import TPDB.Data
+import Data.Typeable
+
+import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
+
+data CertificationProblem =
+     CertificationProblem { input :: CertificationProblemInput 
+                          , cpfVersion :: String -- urgh
+                          , proof :: Proof 
+                          , origin :: Origin  
+                          }  
+   deriving ( Typeable, Eq )
+
+data Origin = ProofOrigin { tool :: Tool }
+    deriving ( Typeable, Eq )
+
+ignoredOrigin = ProofOrigin { tool = Tool "ignored" "ignored"  }
+
+data Tool = Tool { name :: String 
+                 , version :: String
+                 } 
+    deriving ( Typeable, Eq )
+
+data CertificationProblemInput 
+    = TrsInput { trsinput_trs :: TRS Identifier Identifier }
+      -- ^ this is actually not true, since instead of copying from XTC,
+      -- CPF format repeats the definition of TRS,
+      -- and it's a different one (relative rules are extra)
+    | ComplexityInput { trsinput_trs :: TRS Identifier Identifier
+                      , complexityMeasure :: ComplexityMeasure
+                      , complexityClass :: ComplexityClass      
+                      }
+   deriving ( Typeable, Eq )      
+
+data Proof = TrsTerminationProof TrsTerminationProof
+           | TrsNonterminationProof TrsNonterminationProof
+           | RelativeTerminationProof TrsTerminationProof
+           | RelativeNonterminationProof TrsNonterminationProof
+           | ComplexityProof ComplexityProof
+   deriving ( Typeable, Eq )
+
+data DPS = forall s . ( XmlContent s , Typeable s, Eq s ) 
+        => DPS [ Rule (Term Identifier s) ]
+   deriving ( Typeable )
+
+instance Eq DPS where x == y = error "instance Eq DPS"
+
+
+data ComplexityProof = ComplexityProofFIXME ()
+    deriving ( Typeable, Eq )
+
+data ComplexityMeasure 
+     = DerivationalComplexity
+     | RuntimeComplexity
+    deriving ( Typeable, Eq )
+
+data ComplexityClass = 
+     ComplexityClassPolynomial { degree :: Int } 
+     -- ^ it seems the degree must always be given in CPF,
+     -- although the category spec also allows "POLY"
+     -- http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php
+    deriving ( Typeable, Eq )
+
+data TrsNonterminationProof = TrsNonterminationProofFIXME ()
+    deriving ( Typeable, Eq )
+
+data TrsTerminationProof 
+     = RIsEmpty
+     | RuleRemoval { rr_orderingConstraintProof :: OrderingConstraintProof
+                   , trs :: TRS Identifier Identifier 
+                   , trsTerminationProof :: TrsTerminationProof  
+                   }  
+     | DpTrans  { dptrans_dps :: DPS
+                , markedSymbols :: Bool , dptrans_dpProof :: DpProof }
+     | Semlab {  model :: Model 
+              , trs :: TRS Identifier Identifier
+              , trsTerminationProof :: TrsTerminationProof
+              }
+     | Unlab {  trs :: TRS Identifier Identifier
+              , trsTerminationProof :: TrsTerminationProof
+              }
+     | StringReversal { trs :: TRS Identifier Identifier
+                      , trsTerminationProof :: TrsTerminationProof  
+                      }  
+   deriving ( Typeable, Eq )
+
+data Model = FiniteModel Int [Interpret]
+   deriving ( Typeable, Eq )
+       
+data DpProof = PIsEmpty  
+             | RedPairProc { rppOrderingConstraintProof :: OrderingConstraintProof
+                           , rppDps                     :: DPS 
+                           , rppUsableRules             :: Maybe DPS
+                           , rppDpProof                 :: DpProof 
+                           }  
+             | DepGraphProc [ DepGraphComponent ]
+
+             | SemLabProc { slpModel   :: Model
+                          , slpDps     :: DPS
+                          , slpTrs     :: DPS
+                          , slpDpProof :: DpProof
+                          }
+             | UnlabProc  { ulpDps :: DPS
+                          , ulpTrs :: DPS
+                          , ulpDpProof :: DpProof
+                          }
+   deriving ( Typeable, Eq )
+
+data DepGraphComponent =
+     DepGraphComponent { dgcRealScc :: Bool
+                       , dgcDps :: DPS
+                       , dgcDpProof :: DpProof
+                       }
+   deriving ( Typeable, Eq )
+
+data OrderingConstraintProof = OCPRedPair RedPair
+                             deriving ( Typeable, Eq )
+
+data RedPair = RPInterpretation Interpretation
+             | RPPathOrder      PathOrder
+             deriving ( Typeable, Eq )
+
+data Interpretation =
+     Interpretation { interpretation_type :: Interpretation_Type
+                    , interprets :: [ Interpret  ]
+                    }
+   deriving ( Typeable, Eq )
+
+data Interpretation_Type = 
+   Matrix_Interpretation { domain :: Domain, dimension :: Int
+                         , strictDimension :: Int
+                         }
+   deriving ( Typeable, Eq )
+
+data Domain = Naturals 
+            | Rationals Rational
+            | Arctic Domain
+            | Tropical Domain
+   deriving ( Typeable, Eq )
+
+data Interpret = Interpret 
+    { symbol :: Symbol , arity :: Int , value :: Value }
+   deriving ( Typeable, Eq )
+
+data Value = Polynomial    Polynomial
+           | ArithFunction ArithFunction
+   deriving ( Typeable, Eq )
+
+data Polynomial = Sum [ Polynomial ]
+                | Product [ Polynomial ]
+                | Polynomial_Coefficient Coefficient
+                | Polynomial_Variable String
+   deriving ( Typeable, Eq )
+
+data ArithFunction = AFNatural  Integer
+                   | AFVariable Integer
+                   | AFSum      [ArithFunction]
+                   | AFProduct  [ArithFunction]
+                   | AFMin      [ArithFunction]
+                   | AFMax      [ArithFunction]
+                   | AFIfEqual  ArithFunction ArithFunction ArithFunction ArithFunction
+                   deriving ( Typeable, Eq )
+
+data Symbol = SymName  Identifier
+            | SymSharp Symbol
+            | SymLabel Symbol Label
+            deriving ( Typeable, Eq )
+
+data Label = LblNumber [Integer]
+           | LblSymbol [Symbol]
+           deriving ( Typeable, Eq )
+
+data Coefficient = Vector [ Coefficient ]
+           | Matrix [ Coefficient ]
+           | forall a . (Eq a, XmlContent a ) => Coefficient_Coefficient a
+   deriving ( Typeable )
+
+instance Eq Coefficient where x == y = error "instance Eq Coefficient"
+
+data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite
+   deriving ( Typeable, Eq )
+
+class ToExotic a where toExotic :: a -> Exotic
+
+data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
+               deriving ( Typeable, Eq )
+
+data PrecedenceEntry = PrecedenceEntry { peSymbol     :: Symbol
+                                       , peArity      :: Int
+                                       , pePrecedence :: Integer
+                                       }
+                     deriving ( Typeable, Eq )
+
+data ArgumentFilterEntry = 
+     ArgumentFilterEntry { afeSymbol :: Symbol
+                         , afeArity  :: Int
+                         , afeFilter :: Either Int [Int]
+                         }
+     deriving ( Typeable, Eq )
diff --git a/src/TPDB/CPF/Proof/Util.hs b/src/TPDB/CPF/Proof/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/CPF/Proof/Util.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE LambdaCase #-}
+module TPDB.CPF.Proof.Util where
+
+import qualified Data.Map as M
+import           Data.List (nub)
+import           TPDB.Data 
+import           TPDB.CPF.Proof.Type hiding (name)
+import           TPDB.DP 
+
+fromMarkedIdentifier :: Marked Identifier -> Symbol
+fromMarkedIdentifier = \case 
+  Original i -> SymName i
+  Marked i   -> SymSharp $ SymName i
+
+sortVariables :: Rule (Term Identifier s) -> Rule (Term Identifier s)
+sortVariables r = r { lhs = vmap mapVar $ lhs r
+                    , rhs = vmap mapVar $ rhs r
+                    }
+  where
+    oldVars      = nub $ voccs $ lhs r
+    newVars      = zipWith mkNewVar [1..] oldVars
+    mkNewVar i v = v { name = "x" ++ show i }
+    mapping      = M.fromList $ zip oldVars newVars
+    mapVar v     = case M.lookup v mapping of
+      Just v' -> v'
+      Nothing -> error "TPDB.CPF.Proof.Util.sortVariables"
diff --git a/src/TPDB/CPF/Proof/Write.hs b/src/TPDB/CPF/Proof/Write.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/CPF/Proof/Write.hs
@@ -0,0 +1,333 @@
+{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}
+
+-- | from internal representation to XML, and back
+
+module TPDB.CPF.Proof.Write where
+
+import TPDB.CPF.Proof.Type
+import qualified TPDB.Data as T
+
+import qualified Text.XML.HaXml.Escape as E
+import qualified Text.XML.HaXml.Pretty as P
+
+import Text.XML.HaXml.Types (QName (..) )
+import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
+import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..), Misc (PI) )
+
+import TPDB.Xml 
+import TPDB.Data.Xml 
+
+import Data.List ( nub )
+import Data.Char ( toLower )
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import qualified Data.Time as T
+import Control.Monad
+import Data.Typeable
+import Data.Ratio
+
+tox :: CertificationProblem -> Document ()
+tox p = 
+    let xd = XMLDecl "1.0" ( Just $ EncodingDecl "UTF-8" ) Nothing 
+        style = PI ("xml-stylesheet", "type=\"text/xsl\" href=\"cpfHTML.xsl\"")
+        pro = Prolog ( Just xd ) [] Nothing [style]
+        [ CElem e _ ] = toContents p
+    in  Document pro emptyST e []
+
+instance XmlContent CertificationProblem where
+   parseContents = error "parseContents not implemented"
+
+   toContents cp = rmkel "certificationProblem"
+         [ mkel "input" $ toContents ( input cp )
+         , mkel "cpfVersion" [ nospaceString $ cpfVersion cp ]
+         , mkel "proof" $ toContents ( proof cp )
+         , mkel "origin" $ toContents ( origin cp )
+         ]
+
+instance XmlContent Origin where
+   parseContents = error "parseContents not implemented"
+
+   toContents o = case o of
+       ProofOrigin t -> rmkel "proofOrigin" $ toContents t
+
+instance XmlContent Tool where
+   parseContents = error "parseContents not implemented"
+
+   toContents t = rmkel "tool" 
+         [ mkel "name"    [ nospaceString $ name    t ]
+         , mkel "version" [ nospaceString $ version t ]
+         ]
+
+instance XmlContent CertificationProblemInput where
+   parseContents = error "parseContents not implemented"
+
+   toContents i = case i of
+      TrsInput {} -> rmkel "trsInput" $ toContents ( symbolize $ trsinput_trs i )
+      ComplexityInput {} -> rmkel "complexityInput" $ concat
+          [ rmkel "trsInput" $ toContents $ symbolize $ trsinput_trs i
+          ]
+
+instance XmlContent ( T.TRS Identifier Symbol ) where
+   parseContents = error "parseContents not implemented"
+
+   toContents s = rmkel "trs" 
+       $ rmkel "rules" $ concat $ map toContents $ T.rules s
+
+instance ( Typeable t, XmlContent t  ) 
+        => XmlContent ( T.Rule t) where
+   parseContents = error "parseContents not implemented"
+
+   toContents u = rmkel "rule" $ concat
+      [ rmkel "lhs" ( toContents $ T.lhs u )
+      , rmkel "rhs" ( toContents $ T.rhs u )
+      ]
+
+instance XmlContent Proof where
+   parseContents = error "parseContents not implemented"
+
+   toContents p = 
+     let missing t = rmkel t $ rmkel "missing-toContents-instance" [] 
+     in  case p of
+       TrsTerminationProof p -> toContents p
+       TrsNonterminationProof p -> missing "TrsNonterminationProof"
+       RelativeTerminationProof p -> missing "RelativeTerminationProof"
+       RelativeNonterminationProof p -> missing "RelativeNonterminationProof"
+       ComplexityProof p -> missing "ComplexityProof"
+
+instance XmlContent DPS where
+   parseContents = error "parseContents not implemented"
+
+   toContents ( DPS rules ) = rmkel "dps" 
+        $ rmkel "rules" $ rules >>= toContents
+
+instance XmlContent TrsTerminationProof where
+   parseContents = error "parseContents not implemented"
+
+   toContents p = rmkel "trsTerminationProof" $ case p of
+      RIsEmpty -> rmkel "rIsEmpty" []
+      DpTrans {} -> rmkel "dpTrans" $ concat
+          [ toContents $ dptrans_dps p
+          , rmkel "markedSymbols" [ nospaceString "true" ]
+          , toContents $ dptrans_dpProof p
+          ]
+      StringReversal {} -> rmkel "stringReversal" $ concat
+          [ toContents $ symbolize $ trs p
+          , toContents $ trsTerminationProof p
+          ]
+      RuleRemoval {} -> rmkel "ruleRemoval" $ concat
+          [ toContents $ rr_orderingConstraintProof p
+          , toContents $ symbolize $ trs p
+          , toContents $ trsTerminationProof p
+          ]
+
+symbolize trs = 
+    ( fmap (fmap SymName) trs )
+    { T.signature = map SymName $ T.signature trs }
+
+instance XmlContent Model where
+  parseContents = error "parseContents not implemented"
+
+  toContents model = rmkel "model" $ case model of
+    FiniteModel carrierSize interprets ->
+      rmkel "finiteModel" $ concat
+        [ rmkel "carrierSize" [ nospaceString $ show carrierSize ]
+        , concatMap toContents interprets
+        ]
+
+instance XmlContent DpProof where
+  parseContents = error "parseContents not implemented"
+
+  toContents p = rmkel "dpProof" $ case p of
+    PIsEmpty -> rmkel "pIsEmpty" []
+    RedPairProc {} -> case rppUsableRules p of
+      Nothing -> rmkel "redPairProc" $ concat
+        [ toContents $ rppOrderingConstraintProof p
+        , toContents $ rppDps p
+        , toContents $ rppDpProof p
+        ]
+      Just (DPS ur) -> rmkel "redPairUrProc" $ concat
+        [ toContents $ rppOrderingConstraintProof p
+        , toContents $ rppDps p
+        , rmkel "usableRules" $ rmkel "rules" $ concatMap toContents ur
+        , toContents $ rppDpProof p
+        ]
+    DepGraphProc cs -> rmkel "depGraphProc" $ concat $ map toContents cs
+
+    SemLabProc {} -> rmkel "semlabProc" $ concat
+      [ toContents $ slpModel p
+      , toContents $ slpDps p
+      , case slpTrs p of
+          DPS rules -> rmkel "trs" $ rmkel "rules" $ rules >>= toContents
+
+      , toContents $ slpDpProof p
+      ]
+
+    UnlabProc {} -> rmkel "unlabProc" $ concat
+      [ toContents $ ulpDps p
+      , case ulpTrs p of
+          DPS rules -> rmkel "trs" $ rmkel "rules" $ rules >>= toContents
+      , toContents $ ulpDpProof p
+      ]
+
+instance XmlContent DepGraphComponent where
+    toContents dgc = rmkel "component" $ concat $
+        [ {- rmkel "dps" $ -} toContents $ dgcDps dgc
+        , rmkel "realScc" 
+           --  $ toContents $ dgcRealScc dgc
+           -- NO, Bool is encoded as text, not as attribute
+            [ nospaceString $ map toLower $ show $ dgcRealScc dgc ]
+        ] ++ 
+        [ {- rmkel "dpProof" $ -} toContents $ dgcDpProof dgc
+        | dgcRealScc dgc
+        ]
+
+instance XmlContent OrderingConstraintProof where
+  parseContents = error "parseContents not implemented"
+
+  toContents (OCPRedPair rp) = rmkel "orderingConstraintProof" 
+                             $ toContents rp
+           
+instance XmlContent RedPair where
+  parseContents = error "parseContents not implemented"
+
+  toContents rp = rmkel "redPair" $ case rp of
+    RPInterpretation i -> toContents i
+    RPPathOrder      o -> toContents o
+
+instance XmlContent Interpretation where
+   parseContents = error "parseContents not implemented"
+
+   toContents i = rmkel "interpretation" $
+        rmkel "type" ( toContents $ interpretation_type i )
+     ++ concatMap toContents ( interprets i )
+      
+instance XmlContent Interpretation_Type where
+   parseContents = error "parseContents not implemented"
+
+   toContents t = rmkel "matrixInterpretation" $ concat 
+      [ toContents ( domain t )
+      , rmkel "dimension"       [ nospaceString $ show $ dimension t ]
+      , rmkel "strictDimension" [ nospaceString $ show $ strictDimension t ]
+      ]
+     
+instance XmlContent Domain where
+   parseContents = error "parseContents not implemented"
+
+   toContents d = rmkel "domain" $ case d of
+       Naturals -> rmkel "naturals" []
+       Rationals delta -> rmkel "rationals" 
+         $ rmkel "delta" $ toContents delta
+       Arctic d -> rmkel "arctic" $ toContents d
+       Tropical d -> rmkel  "tropical" $ toContents d
+
+instance XmlContent Rational where
+    parseContents = error "parseContents not implemented"
+
+    toContents r = rmkel "rational" 
+        [ mkel "numerator"   [ nospaceString $ show $ numerator   r ]
+        , mkel "denominator" [ nospaceString $ show $ denominator r ]
+        ]
+
+instance XmlContent Interpret  where
+   parseContents = error "parseContents not implemented"
+
+   toContents i = rmkel "interpret" $ concat
+                    [ toContents $ symbol i
+                    , rmkel "arity" [ nospaceString $ show $ arity i ]
+                    , toContents $ value i
+                    ]
+
+instance XmlContent Value where
+   parseContents = error "parseContents not implemented"
+
+   toContents v = case v of
+      Polynomial p -> toContents p
+      ArithFunction f -> toContents f
+
+instance XmlContent Polynomial where
+   parseContents = error "parseContents not implemented"
+
+   toContents p = rmkel "polynomial" $ case p of
+       Sum     ps -> rmkel "sum"     $ concat ( map toContents ps )
+       Product ps -> rmkel "product" $ concat ( map toContents ps )
+       Polynomial_Coefficient c -> rmkel "coefficient" $ toContents c
+       Polynomial_Variable v -> rmkel "variable" [ nospaceString v ]
+
+instance XmlContent ArithFunction where
+  parseContents = error "parseContents not implemented"
+
+  toContents af = rmkel "arithFunction" $ case af of
+    AFNatural  n      -> rmkel "natural"  [ nospaceString $ show n ]
+    AFVariable n      -> rmkel "variable" [ nospaceString $ show n ]
+    AFSum     afs     -> rmkel "sum"      $ concatMap toContents afs
+    AFProduct afs     -> rmkel "product"  $ concatMap toContents afs
+    AFMin     afs     -> rmkel "min"      $ concatMap toContents afs
+    AFMax     afs     -> rmkel "max"      $ concatMap toContents afs
+    AFIfEqual a b t f -> rmkel "ifEqual"  $ concatMap toContents [a,b,t,f]
+
+instance XmlContent Coefficient where
+   parseContents = error "parseContents not implemented"
+
+   toContents v = case v of
+       Matrix vs -> rmkel "matrix" $ concat ( map toContents vs )
+       Vector cs -> rmkel "vector" $ concat ( map toContents cs )
+       Coefficient_Coefficient i -> 
+          rmkel "coefficient" $ toContents i
+
+instance XmlContent Exotic where
+    parseContents = error "parseContents not implemented"
+
+    toContents e = case e of
+       Minus_Infinite -> rmkel "minusInfinity" []
+       E_Integer i -> rmkel "integer" [ nospaceString $ show i ]
+       Plus_Infinite -> rmkel "plusInfinity" []
+
+-- see remark in TPDB.Data.Xml (sharp_name_HACK)
+
+instance XmlContent Symbol where
+  parseContents = error "parseContents not implemented"
+
+  toContents (SymName id) = rmkel "name" [nospaceString $ show id]
+  toContents (SymSharp sym) = rmkel "sharp" $ toContents sym
+  toContents (SymLabel sym label) = rmkel "labeledSymbol" 
+                                  $ toContents sym ++ (toContents label)
+
+instance XmlContent Label where
+  parseContents = error "parseContents not implemented"
+
+  toContents (LblNumber is) = 
+    rmkel "numberLabel" $ map (\i -> mkel "number" [ nospaceString $ show i ]) is
+
+  toContents (LblSymbol ss) = rmkel "symbolLabel" $ concatMap toContents ss
+
+instance XmlContent PathOrder where
+  parseContents = error "parseContents not implemented"
+
+  toContents (PathOrder ps as) = rmkel "pathOrder" $ concat
+    [ rmkel "statusPrecedence" $ concatMap toContents ps
+    , if null as then []
+      else rmkel "argumentFilter" $ concatMap toContents as
+    ]
+
+instance XmlContent PrecedenceEntry where
+  parseContents = error "parseContents not implemented"
+
+  toContents (PrecedenceEntry s a p) = rmkel "statusPrecedenceEntry" $ concat
+    [ toContents s
+    , rmkel "arity"      [ nospaceString $ show a ]
+    , rmkel "precedence" [ nospaceString $ show p ]
+    , rmkel "lex"        [ ]
+    ]
+
+instance XmlContent ArgumentFilterEntry where
+  parseContents = error "parseContents not implemented"
+
+  toContents (ArgumentFilterEntry s a f) = rmkel "argumentFilterEntry" $ concat
+    [ toContents s
+    , rmkel "arity"      [ nospaceString $ show a ]
+    , case f of 
+        Left i   -> rmkel "collapsing" [ nospaceString $ show i ]
+        Right is -> rmkel "nonCollapsing" 
+                  $ map (\i -> mkel "position" [ nospaceString $ show i ]) is
+    ]
diff --git a/src/TPDB/CPF/Proof/Xml.hs b/src/TPDB/CPF/Proof/Xml.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/CPF/Proof/Xml.hs
@@ -0,0 +1,6 @@
+module TPDB.CPF.Proof.Xml 
+( module TPDB.CPF.Proof.Read
+, module TPDB.CPF.Proof.Write 
+) where
+import TPDB.CPF.Proof.Read
+import TPDB.CPF.Proof.Write 
diff --git a/src/TPDB/Convert.hs b/src/TPDB/Convert.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Convert.hs
@@ -0,0 +1,41 @@
+module TPDB.Convert where
+
+import TPDB.Data
+import Control.Monad ( forM, guard )
+
+srs2trs :: SRS Identifier -> TRS Identifier Identifier
+srs2trs s = s { separate = False
+              , rules = map convert_srs_rule $ rules s
+              }  
+
+convert_srs_rule u = 
+    let v = mk 0 "x"
+        set_arity a s = s { arity = a }
+        handle = unspine v . map (set_arity 1)
+    in  u { lhs = handle $ lhs u
+          , rhs = handle $ rhs u        
+          } 
+                  
+trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )
+trs2srs t = do
+    us <- forM ( rules t ) convert_trs_rule 
+    return $ t { separate = True , rules = us }
+
+convert_trs_rule u = do
+      ( left_spine, left_base ) <- spine $ lhs u
+      ( right_spine, right_base ) <- spine $ rhs u
+      guard $ left_base == right_base     
+      return $ u { lhs = left_spine, rhs = right_spine }
+
+unspine :: v -> [s] -> Term v s
+unspine v = foldr (  \ c t -> Node c [ t ] ) ( Var v )
+
+-- | success iff term consists of unary symbols
+-- and the lowest node is a variable
+spine :: Term v s -> Maybe ( [s], v )
+spine t = case t of
+    Node f args -> do
+      [ arg ] <- return args
+      ( sp, base ) <- spine arg 
+      return ( f : sp, base )
+    Var v -> return ( [] , v ) 
diff --git a/src/TPDB/DP.hs b/src/TPDB/DP.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/DP.hs
@@ -0,0 +1,7 @@
+module TPDB.DP ( module TPDB.DP.Transform )
+
+where
+
+import TPDB.DP.Transform
+import TPDB.DP.Graph
+
diff --git a/src/TPDB/DP/Graph.hs b/src/TPDB/DP/Graph.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/DP/Graph.hs
@@ -0,0 +1,53 @@
+module TPDB.DP.Graph where
+
+import TPDB.DP.TCap
+import TPDB.DP.Unify
+import TPDB.DP.Transform 
+
+import TPDB.Data
+import TPDB.Pretty
+
+import TPDB.Plain.Read -- for testing
+import TPDB.Plain.Write -- for testing
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+import Data.Graph ( stronglyConnComp, SCC(..) )
+import Control.Monad ( guard, forM )
+import Control.Applicative
+
+import Control.Monad.State.Strict 
+
+
+-- | DP problems for strongly connected components, 
+-- topologically sorted, with CyclicComponents in Right,
+-- others in Left.
+components s = do 
+    let es = M.fromListWith (++) 
+           $ do (p,q) <- edges s ; return (p, [q])
+        key = M.fromList 
+            $ zip (filter strict $ rules s) [0.. ]
+    comp <- reverse $ stronglyConnComp $ do
+        p <- M.keys key
+        let qs = M.findWithDefault [] p es
+        return (p, key M.! p, map (key M.!) qs )
+    return $ case comp of
+        CyclicSCC vs -> Right $ s { rules = vs 
+                 ++ filter (not . strict) (rules s) } 
+        AcyclicSCC v -> Left v
+
+-- | edges of the estimated dependency graph
+edges s = do
+    let def = S.filter isOriginal $ defined s
+    u <- filter strict $ rules s
+    v <- filter strict $ rules s
+    guard $ unifies ( vmap Left $ tcap s $ rhs u ) 
+                    ( vmap Right $ lhs v )
+    return (u,v)
+
+check = edges $ dp sys
+
+-- example from "DP Revisited" http://colo6-c703.uibk.ac.at/ttt/rta04.pdf
+Right sys = 
+    TPDB.Plain.Read.trs "(VAR x y) (RULES not(not(x)) -> x not(or(x,y)) -> and(not(x),not(y)) not(and(x,y)) -> or (not(x),not(y)) and(x,or(y,z)) -> or(and(x,z),and(y,z)) and(or(y,z),x) -> or(and(x,y),and(x,z)))"
+
diff --git a/src/TPDB/DP/TCap.hs b/src/TPDB/DP/TCap.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/DP/TCap.hs
@@ -0,0 +1,29 @@
+module TPDB.DP.TCap where
+
+import TPDB.Data
+import TPDB.Pretty
+
+import TPDB.DP.Unify
+
+import Control.Monad.State.Strict 
+import Control.Applicative
+
+
+-- |  This function keeps only those parts of the input term which cannot be reduced,
+-- even if the term is instantiated. All other parts are replaced by fresh variables.
+-- Def 4.4 in http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf
+
+tcap :: (Ord v, Ord c) => TRS v c -> Term v c -> Term Int c
+tcap dp t = evalState ( walk dp t ) 0
+
+fresh_var :: State Int ( Term Int c )
+fresh_var = do i <- get ; put $ succ i ; return $ Var i
+
+walk dp t = case t of
+    Node f args -> do
+        t' <- Node f <$> forM args (walk dp)
+        if all ( \ u -> not $ unifies ( vmap Left $ lhs u ) ( vmap Right t' ) )
+                   $ filter (not . strict) $ rules dp
+            then return t' else fresh_var
+    _ -> fresh_var 
+
diff --git a/src/TPDB/DP/Transform.hs b/src/TPDB/DP/Transform.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/DP/Transform.hs
@@ -0,0 +1,71 @@
+{-# language OverloadedStrings #-}
+{-# LANGUAGE DeriveGeneric #-}
+
+module TPDB.DP.Transform  where
+
+import TPDB.Data
+import TPDB.Pretty
+
+import qualified Data.Set as S
+import Control.Monad ( guard, forM )
+
+import Data.Hashable
+import GHC.Generics
+
+data Marked a = Original a | Marked a | Auxiliary a
+    deriving ( Show, Eq, Ord, Generic )
+
+isOriginal m = case m of Original {} -> True ; _ -> False
+isMarked   m = case m of Marked   {} -> True ; _ -> False
+
+instance Hashable a => Hashable (Marked a) 
+
+instance Pretty a => Pretty ( Marked a) where
+   pretty m = case m of
+       Original a -> pretty a
+       Marked a -> pretty a <> "#"
+       Auxiliary a -> pretty a
+
+mark_top :: Term v a -> Term v (Marked a)
+mark_top  (Node f args) = 
+          Node (Marked f) $ map (fmap Original) args
+
+defined s = S.fromList $ do 
+                u <- rules s
+                let Node f args = lhs u
+                -- will raise exception if lhs is variable
+                return f
+
+-- | compute the DP transformed system.
+
+dp :: (Ord v, Ord s) 
+   => RS s (Term v s) 
+   -> RS (Marked s) (Term v (Marked s))
+dp s = 
+   let os = map ( \ u -> Rule { relation = Weak
+                               , lhs = fmap Original $ lhs u  
+                               , rhs = fmap Original $ rhs u  
+                               , top = False
+                               } )
+           $ rules s
+       def = defined s
+       us = do 
+            u <- rules s
+            let ssubs = S.fromList $ strict_subterms $ lhs u
+                walk r = if S.member r ssubs then [] else case r of
+                    -- will raise exception if rhs contains 
+                    -- a variable that is not in lhs
+                    Node f args -> 
+                        ( if S.member f def then (r :) else id )
+                        ( args >>= walk )
+            r <- walk $ rhs u
+            return $ Rule { relation = Strict
+                          , lhs = mark_top $ lhs u
+                          , rhs = mark_top r 
+                          , top = True
+                          }
+   in RS { signature = map Marked ( S.toList def )
+                     ++ map Original ( signature s )
+         , rules = us ++ os
+         , separate = separate s 
+         } 
diff --git a/src/TPDB/DP/Unify.hs b/src/TPDB/DP/Unify.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/DP/Unify.hs
@@ -0,0 +1,57 @@
+module TPDB.DP.Unify ( mgu, match, unifies, apply, times ) where
+
+import TPDB.Data
+import qualified Data.Map as M
+import Control.Monad ( guard, foldM )
+import Data.Maybe (isJust)
+
+type Substitution v c = M.Map v (Term v c)
+
+unifies t1 t2 = isJust $ mgu t1 t2
+
+-- | view variables as symbols
+pack :: Term v c -> Term any (Either v c)
+pack ( Var v ) = Node ( Left v ) []
+pack ( Node f args ) = Node ( Right f ) ( map pack args )
+
+unpack :: Term any (Either v c) -> Term v c
+unpack ( Node ( Left v ) [] ) = Var v
+unpack ( Node ( Right f ) args ) = Node f ( map unpack args )
+
+-- | will only bind variables in the left side
+match :: ( Ord v, Ord w, Eq c )
+      => Term v c
+      -> Term w c
+      -> Maybe ( M.Map v ( Term w c ) )
+match l r = do
+    u <- mgu ( fmap Right l ) ( pack r )
+    return $ M.map unpack  u
+
+
+-- | naive implementation (worst case exponential)
+mgu
+  :: (Ord v, Eq c) =>
+     Term v c -> Term v c -> Maybe (M.Map v (Term v c))
+mgu t1 t2 | t1 == t2 = return M.empty
+mgu ( Var v ) t2 = do
+    guard $ not $ elem (Var v) $ subterms t2
+    return $ M.singleton v t2
+mgu t1 ( Var v ) = mgu ( Var v ) t1  
+mgu (Node f1 args1) (Node f2 args2) 
+    | f1 == f2 && length args1 == length args2 = do
+        guard $ f1 == f2
+        foldM ( \ s (l,r) -> do
+            t <- mgu (apply l s) (apply r s) 
+            return $ times s t ) M.empty $ zip args1 args2 
+mgu _ _ = Nothing
+   
+times :: Ord v 
+      => Substitution v c -> Substitution v c -> Substitution v c
+times s t = 
+    M.union ( M.difference t s )
+            ( M.map ( \ v -> apply v t ) s )
+
+apply t s = case t of
+    Var v -> case  M.lookup v s of Nothing -> t ; Just w -> w
+    Node f args -> Node f $ map (\ a -> apply a s) args
+    
diff --git a/src/TPDB/DP/Usable.hs b/src/TPDB/DP/Usable.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/DP/Usable.hs
@@ -0,0 +1,43 @@
+module TPDB.DP.Usable where
+
+import TPDB.Data
+import TPDB.Pretty
+
+import TPDB.DP.Unify
+import TPDB.DP.TCap
+
+import qualified Data.Set as S
+
+-- | DANGER: this ignores the CE condition
+restrict :: (Ord c, Ord v) => RS c (Term v c) -> RS c (Term v c)
+restrict dp = 
+    dp { rules = filter strict (rules dp)
+               ++ S.toList ( usable dp)
+       }
+
+-- | computes the least closed set of usable rules, cf. Def 4.5
+-- http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf
+
+usable ::   (Ord v, Ord c)
+       => TRS v c -> S.Set (Rule (Term v c))
+usable dp = fixpoint ( \ s -> S.union s $ required dp s)
+    (required dp $ S.filter strict
+                 $ S.fromList $ rules dp) 
+
+fixpoint f x = 
+    let y = f x in if x == y then x else fixpoint f y
+
+required ::  (Ord v, Ord c)
+       => TRS v c -> S.Set ( Rule (Term v c) ) ->  S.Set ( Rule (Term v c) ) 
+required dp rs = 
+    S.fromList $ do { r <- S.toList rs ;  needed dp $ rhs r }
+
+needed :: (Ord v, Ord c)
+       => TRS v c -> Term v c -> [ Rule (Term v c) ]
+needed dp t = case t of
+    Node f args -> 
+          filter ( \ u -> unifies ( vmap Left $ lhs u ) ( vmap Right $ tcap dp t ) )
+                ( filter (not . strict) $ rules dp )
+        ++ ( args >>= needed dp )
+    Var v -> []
+
diff --git a/src/TPDB/Data.hs b/src/TPDB/Data.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Data.hs
@@ -0,0 +1,121 @@
+{-# language DeriveDataTypeable #-}
+
+module TPDB.Data 
+
+( module TPDB.Data
+, module TPDB.Data.Term
+)
+
+where
+
+
+import TPDB.Data.Term
+
+import Data.Typeable
+import Control.Monad ( guard )
+
+import Data.Hashable
+import Data.Function (on)
+
+data Identifier = 
+     Identifier { _identifier_hash :: ! Int
+                , name :: ! String 
+                , arity :: Int 
+                }
+    deriving ( Eq, Ord, Typeable )
+
+instance Hashable Identifier where
+    hashWithSalt s i = hash (s, _identifier_hash i)
+
+instance Show Identifier where show = name
+
+mk :: Int -> String -> Identifier
+mk a n = Identifier { _identifier_hash = hash (a,n)
+                    , arity = a, name = n }
+
+
+---------------------------------------------------------------------
+
+data Relation = Strict |  Weak | Equal deriving ( Eq, Ord, Typeable, Show )
+
+data Rule a = Rule { lhs :: a, rhs :: a 
+                   , relation :: Relation
+                   , top :: Bool
+                   }
+    deriving ( Eq, Ord, Typeable )
+
+strict :: Rule a -> Bool
+strict u = case relation u of Strict -> True ; _ -> False
+
+weak :: Rule a -> Bool
+weak u = case relation u of Weak -> True ; _ -> False
+
+equal :: Rule a -> Bool
+equal u = case relation u of Equal -> True ; _ -> False
+
+instance Functor (RS s) where
+    fmap f rs = rs { rules = map (fmap f) $ rules rs }
+
+instance Functor Rule where 
+    fmap f u = u { lhs = f $ lhs u, rhs = f $ rhs u } 
+
+data RS s r = 
+     RS { signature :: [ s ] -- ^ better keep order in signature (?)
+         , rules :: [ Rule r ]
+        , separate :: Bool -- ^ if True, write comma between rules
+         }
+   deriving ( Typeable )
+
+instance Eq r => Eq (RS s r) where
+    (==) = (==) `on` rules
+
+strict_rules sys = 
+    do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
+weak_rules sys = 
+    do u <- rules sys ; guard $ weak u ; return ( lhs u, rhs u )
+equal_rules sys = 
+    do u <- rules sys ; guard $ equal u ; return ( lhs u, rhs u )
+
+type TRS v s = RS s ( Term v s )
+
+type SRS s = RS s [ s ]
+
+data Problem v s = 
+     Problem { type_ :: Type 
+             , trs :: TRS v s
+             , strategy :: Maybe Strategy
+             -- , metainformation :: Metainformation
+             , startterm :: Maybe Startterm  
+             }
+
+data Type = Termination | Complexity
+     deriving Show 
+
+data Strategy = Full | Innermost | Outermost
+     deriving Show
+
+data Startterm = 
+       Startterm_Constructor_based
+       | Startterm_Full
+     deriving Show     
+
+------------------------------------------------------
+
+-- | legaca stuff (used in matchbox)
+
+type TES = TRS Identifier Identifier
+type SES = SRS Identifier
+
+mknullary s = mk 0 s
+mkunary   s = mk 1 s
+
+from_strict_rules :: Bool -> [(t,t)] -> RS i t
+from_strict_rules sep rs = 
+    RS { rules = map ( \ (l,r) ->
+             Rule { relation = Strict, top = False, lhs = l, rhs = r } ) rs
+       , separate = sep 
+       }
+
+with_rules sys rs = sys { rules = rs }
+
+
diff --git a/src/TPDB/Data/Term.hs b/src/TPDB/Data/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Data/Term.hs
@@ -0,0 +1,166 @@
+{-# language DeriveDataTypeable #-}
+
+module TPDB.Data.Term where
+
+import qualified Data.Set as S
+import Data.Set (Set)
+import Data.Typeable
+
+data Term v s = Var v 
+              | Node s [ Term v s ]
+    deriving ( Eq, Ord, Show, Typeable )
+
+vmap :: ( v -> u ) -> Term v s -> Term u s
+vmap f ( Var v ) = Var ( f v )
+vmap f ( Node c args ) = Node c $ map ( vmap f ) args
+
+instance Functor ( Term v ) where
+    fmap f ( Var v ) = Var v
+    fmap f ( Node c args ) = Node (f c) ( map ( fmap f ) args )
+
+
+
+type Position = [ Int ]
+
+positions :: Term v c 
+          -> [ ( Position, Term v c ) ]
+positions t = ( [], t ) : case t of
+    Node c args -> do ( k, arg ) <- zip [ 0 .. ] args
+		      ( p, s   ) <- positions arg
+		      return ( k : p , s )
+    _ -> []
+
+-- | all positions
+pos :: Term v c 
+    -> [ Position ]
+pos t = do
+    ( p, s ) <- positions t
+    return p
+
+-- | non-variable positions
+sympos :: Term v c 
+    -> [ Position ]
+sympos t = do
+    ( p, Node {} ) <- positions t
+    return p
+
+-- | variable positions
+varpos :: Term v c 
+    -> [ Position ]
+varpos t = do
+    ( p, Var {} ) <- positions t
+    return p
+
+-- | leaf positions (= nullary symbols)
+leafpos :: Term v c 
+    -> [ Position ]
+leafpos t = do
+    ( p, Node c [] ) <- positions t
+    return p
+
+
+{-# inline subterms #-}
+
+subterms :: Term v c 
+	 -> [ Term v c ]
+subterms t = t : case t of
+    Node c args -> do arg <- args
+		      subterms arg
+    _ -> []
+
+-- Note: following implementation relies on @subterms@
+-- returning the preorder list (where the full term goes first)
+strict_subterms t = tail $ subterms t
+
+isSubtermOf :: (Eq v, Eq c ) 
+         => Term v c ->  Term v c  -> Bool
+isSubtermOf s t = elem s $ subterms t
+
+isStrictSubtermOf :: (Eq v, Eq c ) 
+         => Term v c ->  Term v c  -> Bool
+isStrictSubtermOf s t = elem s $ strict_subterms t
+
+-- | compute new symbol at position, giving the position
+pmap:: ( Position -> c -> d )
+     -> Term v c
+     -> Term v d
+pmap f = rpmap ( \ p c -> f ( reverse p) c )
+
+-- | compute new symbol from *reverse* position and previous symbol
+-- this is more efficient (no reverse needed)
+rpmap :: ( Position -> c -> d )
+     -> Term v c
+     -> Term v d
+rpmap f t = helper [] t where
+    helper p ( Node c args ) = Node ( f p c ) $ do
+	     ( k, arg ) <- zip [0..] args
+	     return $ helper ( k : p ) arg
+    helper p ( Var v) = Var v
+
+
+
+peek :: Term v c 
+     -> Position 
+     -> Term v c
+peek t [] = t
+peek ( Node c args ) ( k : ks ) = peek ( args !! k ) ks
+
+peek_symbol :: Term v c 
+     -> Position 
+     -> c
+peek_symbol t p = 
+    case peek t p of
+         Node c args -> c
+	 _ -> error "Autolib.TES.Position.peek_symbol called for non-symbol"
+
+-- | warning: don't check arity
+poke_symbol ::  Term v c 
+     -> ( Position , c )
+     -> Term v c
+poke_symbol t ( p, c ) =  
+    case peek t p of
+         Node _ args -> poke t ( p, Node c args )
+	 _ -> error "Autolib.TES.Position.poke_symbol called for non-symbol"
+
+poke :: Term v c 
+     -> ( Position , Term v c )
+     -> Term v c
+poke t ( [], s ) = s
+poke (Node c args) (k : ks, s ) = 
+    let ( pre , this : post ) = splitAt k args
+    in Node c ( pre ++ poke this ( ks, s ) : post )
+
+pokes :: Term v c
+      -> [ ( Position, Term v c ) ]
+      -> Term v c
+pokes = foldl poke
+
+
+-- | in preorder 
+symsl :: Term v c -> [ c ]
+symsl t = do
+    Node c _ <- subterms t
+    return c
+
+syms :: Ord c => Term v c -> Set c
+syms = S.fromList . symsl
+
+
+lsyms :: Ord c => Term v c -> [ c ]
+lsyms = S.toList . syms
+
+vars :: Ord v => Term v c -> Set v
+vars t = S.fromList $ do
+    Var v <- subterms t
+    return v
+
+isvar :: Term v c -> Bool
+isvar ( Var _ ) = True ; isvar _ = False
+
+-- | list of variables (each occurs once, unspecified ordering)
+lvars :: Ord v => Term v c -> [ v ]
+lvars = S.toList . vars
+
+-- | list of variables (in pre-order, with duplicates)
+voccs :: Term v c -> [ v ]
+voccs t = do ( p, Var v ) <- positions t ; return v
diff --git a/src/TPDB/Data/Xml.hs b/src/TPDB/Data/Xml.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Data/Xml.hs
@@ -0,0 +1,81 @@
+{-# language FlexibleContexts #-}
+{-# language FlexibleInstances #-}
+{-# language UndecidableInstances #-}
+
+module TPDB.Data.Xml where
+
+import TPDB.Data
+import TPDB.Xml
+
+import Text.XML.HaXml.Types (QName (..) )
+import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
+
+import Data.Typeable
+
+-- | FIXME: move to separate module
+instance XmlContent Identifier where
+    parseContents = do
+        CString _ s _ <- next 
+        return  $ mknullary s
+    toContents i =
+          -- probably not here: E.xmlEscape E.stdXmlEscaper
+          -- this introduces whitespace between &lt; and =
+          -- [ CString False $ show i ]
+          -- and this creates a CDATA element
+          -- [ CString True $ show i ]
+          -- so here comes an UGLY HACK:
+          [ CString False ( escape $ show i ) () ]
+
+
+instance ( Typeable ( Term v c ) , XmlContent v, XmlContent c )
+         => XmlContent ( Term v c ) where
+    toContents ( Var v ) = rmkel "var" $ toContents v
+{-
+-- for Rainbow:
+    toContents ( Node f xs ) = return $ mkel "app"
+         $ mkel "fun" ( toContents f )
+         : map ( \ x -> mkel "arg" $ toContents x ) xs
+-}
+-- for CPF:
+
+-- the problem is this:
+-- a variable is an Identifier, and must look like "<var>foo</var>"
+-- a constructor symbol is also an Identifier
+-- but it must look like "<funapp><name>bar<name>..."
+-- so it should be wrapped into <name>
+-- but no, if the constructor is sharped (or labelled)
+-- then it must look like "<funapp><sharp><name>bar..."
+-- price question: what is the correct 
+-- instance XmlContent Identifier ?
+-- the answer probably is "there is none",
+-- and toContents (Term v Identifier) should never occur,
+-- instead need to call  toContents (Term v Symbol)
+
+    toContents ( Node f args ) = rmkel "funapp" 
+            $ no_sharp_name_HACK ( toContents f )
+           ++ map ( \ arg -> mkel "arg" $ toContents arg ) args
+
+no_sharp_name_HACK e = e
+
+sharp_name_HACK e = case e of
+    [ CElem ( Elem (N "sharp") [] cs ) () ] -> 
+        rmkel "sharp" $ rmkel "name" cs
+    _ -> rmkel "name" e
+
+
+
+
+instance HTypeable ( Rule ( Term v c )) where
+     toHType _ = Prim "Rule" "Rule"
+
+instance ( HTypeable ( Rule ( Term v c) )
+         , XmlContent ( Term v c ) ) 
+         => XmlContent ( Rule ( Term v c ) ) where
+    toContents u =
+        return $ mkel "rule" 
+               [ mkel "lhs" $ toContents $ lhs u
+               , mkel "rhs" $ toContents $ rhs u
+               ]
+
+
+
diff --git a/src/TPDB/Input.hs b/src/TPDB/Input.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Input.hs
@@ -0,0 +1,64 @@
+module TPDB.Input where
+
+import TPDB.Data
+import TPDB.Plain.Read
+import TPDB.XTC.Read
+import TPDB.Convert
+
+import System.FilePath.Posix ( takeExtension )
+
+-- | read input from file with given name.
+-- can have extension .srs, .trs, .xml.
+-- unknown extension is considered as .xml, because of 
+-- http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks
+
+get :: FilePath 
+         -> IO ( Either (TRS Identifier Identifier) 
+                        ( SRS Identifier ) )
+get f = do
+    m <- getE f
+    case m of
+        Right x -> return x 
+        Left err -> error err
+
+getE f = case takeExtension f of
+      ".srs" -> do
+          s <- readFile f    
+          case srs s of
+              Left err -> return $ Left err
+              Right t -> return $ Right $ Right t
+      ".trs" -> do        
+          s <- readFile f
+          case TPDB.Plain.Read.trs s of
+              Left err -> return $ Left err
+              Right t -> return $ Right $ Left t 
+      _ -> do
+          ps <- readProblems f
+          case ps of 
+              [ p ] -> return $ Right $ Left $ TPDB.Data.trs p
+              [] -> return $ Left "no TRS"
+              _ -> return $ Left "more than one TRS"
+
+get_trs f = do
+    x <- get f
+    return $ case x of
+        Right x -> srs2trs x
+        Left  x -> x
+
+getE_trs f = do
+    e <- getE f
+    return $ case e of
+        Right x -> Right $ case x of
+            Right x -> srs2trs x
+            Left  x -> x
+        Left e -> Left e
+
+get_srs f = do
+    x <- get f
+    return $ case x of
+        Right x -> x
+        Left  x -> case trs2srs x of
+            Nothing -> error "not an SRS"
+            Just x -> x
+            
+
diff --git a/src/TPDB/Mirror.hs b/src/TPDB/Mirror.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Mirror.hs
@@ -0,0 +1,19 @@
+module TPDB.Mirror where
+
+import TPDB.Data
+import TPDB.Convert
+
+import Control.Monad ( forM, guard )
+
+-- | if input is SRS, reverse lhs and rhs of each rule
+mirror :: TRS Identifier s 
+       -> Maybe ( TRS Identifier s )
+mirror trs = do
+    us <- forM (rules trs) $ \ u -> do
+      ( left_spine, left_base ) <- spine $ lhs u
+      ( right_spine, right_base ) <- spine $ rhs u
+      guard $ left_base == right_base 
+      return $ u { lhs = unspine left_base $ reverse left_spine
+                 , rhs = unspine right_base $ reverse right_spine
+                 }
+    return $ trs { rules = us }
diff --git a/src/TPDB/Plain/Read.hs b/src/TPDB/Plain/Read.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Plain/Read.hs
@@ -0,0 +1,146 @@
+-- | textual input,
+-- cf. <http://www.lri.fr/~marche/tpdb/format.html>
+
+{-# language PatternSignatures, TypeSynonymInstances, FlexibleInstances #-}
+
+module TPDB.Plain.Read where
+
+import TPDB.Data
+
+import Text.Parsec
+import Text.Parsec.Token
+import Text.Parsec.Language
+import Text.Parsec.Char
+
+import TPDB.Pretty (pretty)
+import TPDB.Plain.Write ()
+
+import Control.Monad ( guard, void )
+import Data.List ( nub )
+
+trs :: String -> Either String ( TRS Identifier Identifier )
+trs s = case Text.Parsec.parse reader "input" s of
+    Left err -> Left $ show err
+    Right t  -> Right t
+
+srs :: String -> Either String ( SRS Identifier )
+srs s = case Text.Parsec.parse reader "input" s of
+    Left err -> Left $ show err
+    Right t  -> Right t
+
+type Parser = Parsec String () 
+
+class Reader a where reader :: Parser a
+
+-- | warning: by definition, {}[] may appear in identifiers
+lexer = makeTokenParser
+    $ emptyDef
+       { identStart  = alphaNum <|> oneOf "_:!#$%&*+./<=>?@\\^|-~{}[]'"
+       , identLetter = alphaNum <|> oneOf "_:!#$%&*+./<=>?@\\^|-~{}[]'"
+       , commentLine = "" , commentStart = "" , commentEnd = ""
+       , reservedNames = [ "VAR", "THEORY", "STRATEGY", "RULES", "->", "->=" ]
+       }
+
+
+instance Reader Identifier where 
+    reader = do
+        i <- identifier lexer 
+	return $ mk 0 i
+
+instance Reader s =>  Reader [s] where
+    reader = many reader
+
+-- NOTE: this is dangerous since we read the variables as constants,
+-- and this needs to be patched up later.
+-- NOTE: this is more dangerous as we do not set the arity of identifiers
+instance ( Reader v ) => Reader ( Term v Identifier ) where
+    reader = do
+        f  <- reader 
+        xs <- option [] $ parens lexer $ commaSep lexer reader
+        return $ Node ( f { arity = length xs } ) xs
+
+instance Reader u => Reader ( Rule u ) where
+    reader = do
+        l <- reader
+        rel <-  do reservedOp lexer "->"  ; return Strict
+          <|> do reservedOp lexer "->=" ; return Weak
+          -- FIXME: for the moment, we do not parse this
+          -- as it would deviate from published TPDB syntax
+          -- <|> do reservedOp lexer "=" ; return Equal
+        r <- reader
+        return $ Rule { lhs = l, relation = rel, top = False, rhs = r }
+
+data Declaration u
+     = Var_Declaration [ Identifier ]
+     | Theory_Declaration 
+     | Strategy_Declaration 
+     | Rules_Declaration [ Rule u ]
+     | Unknown_Declaration
+       -- ^ this is super-ugly: a parenthesized, possibly nested, 
+       -- possibly comma-separated, list of identifiers or strings
+
+declaration :: Reader u => Bool -> Parser ( Declaration u )
+declaration sep = parens lexer $ 
+           do reserved lexer "VAR" ; xs <- many reader 
+              return $ Var_Declaration xs
+       <|> do reserved lexer "THEORY" 
+              error "TPDB.Plain.Read: parser for THEORY decl. missing"
+       <|> do reserved lexer "STRATEGY" 
+              error "TPDB.Plain.Read: parser for THEORY decl. missing"
+       <|> do reserved lexer "RULES" 
+              us <- if sep then do 
+                        many $ do 
+                            u <- reader ; optional $ comma lexer
+                            return u
+                        -- yes, TPDB contains some trailing commas, e.g., z008
+                        -- ( RULES a b -> b a , )
+                    else many reader
+              return $ Rules_Declaration us
+       <|> do anylist ; return Unknown_Declaration
+
+anylist = void 
+        $ commaSep lexer 
+        $ many ( void ( identifier lexer ) <|> parens lexer anylist )
+
+instance Reader ( SRS Identifier ) where
+    reader = do 
+        many space
+        ds <- many $ declaration True
+	return $ make_srs ds
+
+instance Reader ( TRS Identifier Identifier ) where
+    reader = do
+        many space
+        ds <- many $ declaration False
+	return $ make_trs ds
+
+repair_signature_srs sys = 
+    let sig = nub $ do u <- rules sys ; lhs u ++ rhs u
+    in  sys { signature = sig }
+
+make_srs :: Eq s => [ Declaration [s] ] -> SRS s
+make_srs ds = repair_signature_srs $
+    let us = do Rules_Declaration us <- ds ; us        
+    in  RS { rules = us, separate = True }
+
+repair_signature_trs sys = 
+    let sig = nub $ do u <- rules sys ; lsyms ( lhs u ) ++ lsyms ( rhs u)
+    in  sys { signature = sig }
+
+make_trs :: [ Declaration ( Term Identifier Identifier ) ] 
+         -> TRS Identifier Identifier
+make_trs ds = repair_signature_trs $
+    let vs = do Var_Declaration vs <- ds ; vs
+        us = do Rules_Declaration us <- ds ; us
+        us' = repair_variables vs us
+    in  RS { rules = us', separate = False }
+
+
+repair_variables vars rules = do
+    let xform ( Node c [] ) | c `elem` vars = Var c
+	xform ( Node c args ) = Node c ( map xform args )
+    rule <- rules  
+    return $ rule { lhs = xform $ lhs rule
+		  , rhs = xform $ rhs rule
+		  }
+
diff --git a/src/TPDB/Plain/Write.hs b/src/TPDB/Plain/Write.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Plain/Write.hs
@@ -0,0 +1,67 @@
+-- | the "old" TPDB format 
+-- cf. <http://www.lri.fr/~marche/tpdb/format.html>
+
+{-# language FlexibleContexts #-}
+{-# language OverloadedStrings #-}
+
+module TPDB.Plain.Write where
+
+import TPDB.Data
+import TPDB.Pretty
+
+import Data.List ( nub )
+import Data.String ( fromString )
+
+instance Pretty Identifier where
+    pretty i = fromString $ name i
+
+instance ( Pretty v, Pretty s ) => Pretty ( Term v s ) where
+    pretty t = case t of
+        Var v -> pretty v
+        Node f xs -> case xs of
+            [] -> pretty f 
+            _  -> pretty f <+> parens ( fsep $ punctuate comma $ map pretty xs )
+
+instance PrettyTerm a => Pretty ( Rule a ) where
+    pretty u = hsep [ prettyTerm $ lhs u
+                    , case relation u of 
+                         Strict -> "->" 
+                         Weak -> "->="
+                         Equal -> "="
+                    -- FIXME: implement "top" annotation
+                    , prettyTerm $ rhs u
+                    ]
+
+class PrettyTerm a where 
+    prettyTerm :: a -> Doc
+
+instance Pretty s => PrettyTerm [s] where    
+    prettyTerm xs = hsep $ map pretty xs
+
+instance ( Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where
+    prettyTerm = pretty
+
+instance ( Pretty s, PrettyTerm r ) => Pretty ( RS s r ) where
+    pretty sys = vcat 
+        [ parens $ "RULES" <+>
+          vcat ( ( if separate sys then punctuate comma else id )
+                 $ map pretty $ rules sys 
+               )
+        -- FIXME: variables are not shown (and it is impossible to compute
+        -- them here, this is actually a TPDB format design error, 
+        -- since variables should be local (per rule), not global)
+        -- FIXME: output strategy, theory
+        ]
+
+instance ( Pretty s, Pretty r ) => Pretty ( Problem s r ) where
+    pretty p = vcat
+       [ pretty $ trs p 
+       , case strategy p of  
+             Nothing -> empty
+             Just s -> fsep [ "strategy"
+                            , fromString ( show s ) ]
+       , case startterm p of  
+             Nothing -> empty
+             Just s -> fsep [ "startterm"
+                            , fromString ( show s ) ] 
+       ]
diff --git a/src/TPDB/Pretty.hs b/src/TPDB/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Pretty.hs
@@ -0,0 +1,59 @@
+module TPDB.Pretty 
+
+( Doc, SimpleDoc
+, render, renderCompact, displayIO
+, Pretty (..)
+, fsep , hsep, vsep, vcat, hcat
+, parens, brackets, angles, braces, enclose
+, punctuate, comma, nest
+, empty, text
+, (<>), (<+>), ($$)
+)
+
+where
+
+import Text.PrettyPrint.Leijen.Text 
+    hiding ( text, (<+>), vcat )
+import qualified Text.PrettyPrint.Leijen.Text 
+import Data.String ( fromString )
+
+-- class Pretty a where pretty :: a -> Doc
+
+fsep = fillSep
+($$) = (<$$>)
+x <+> y = x Text.PrettyPrint.Leijen.Text.<+> align y
+vcat = align . Text.PrettyPrint.Leijen.Text.vcat
+
+render :: Doc -> String
+render = show
+
+text :: String -> Doc
+text = fromString
+
+{-
+
+instance Pretty Int where pretty = text . show
+
+instance ( Pretty a, Pretty b ) => Pretty (a,b) where
+    pretty (x,y) = parens $ fsep $ punctuate comma [ pretty x, pretty y ]
+
+instance ( Pretty a, Pretty b, Pretty c ) => Pretty (a,b,c) where
+    pretty (x,y,z) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z ]
+-}
+
+instance ( Pretty a, Pretty b, Pretty c, Pretty d ) => Pretty (a,b,c,d) where
+    pretty (x,y,z,u) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z, pretty u ]
+
+{-
+instance Pretty a => Pretty [a]  where
+    pretty xs = brackets $ fsep $ punctuate comma $ map pretty xs
+
+instance Pretty a => Pretty (Maybe a) where
+    pretty m = case m of
+        Nothing -> text "Nothing"
+        Just x -> text "Just" <+> pretty x -- FIXME: parens missing
+-}
+
+instance ( Pretty a, Pretty b ) => Pretty (Either a b) where
+    pretty (Left x) = text "Left" <+> parens (pretty x)
+    pretty (Right x) = text "Right" <+> parens (pretty x)
diff --git a/src/TPDB/XTC.hs b/src/TPDB/XTC.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/XTC.hs
@@ -0,0 +1,12 @@
+module TPDB.XTC 
+
+( module TPDB.Data
+, module TPDB.XTC.Read
+)
+
+
+where
+
+import TPDB.Data
+import TPDB.XTC.Read
+
diff --git a/src/TPDB/XTC/Read.hs b/src/TPDB/XTC/Read.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/XTC/Read.hs
@@ -0,0 +1,109 @@
+{-# language Arrows, NoMonomorphismRestriction, PatternSignatures #-}
+
+-- | construct data object from XML tree.
+
+module TPDB.XTC.Read where
+
+-- implementations follows these examples:
+-- http://www.haskell.org/haskellwiki/HXT/Practical/
+
+import TPDB.Data
+
+import Text.XML.HXT.Arrow.XmlArrow
+
+import Text.XML.HXT.Arrow.XmlState ( runX )
+import Text.XML.HXT.Arrow.ReadDocument ( readString )
+import Text.XML.HXT.Arrow.XmlOptions ( a_validate )
+import Text.XML.HXT.DOM.XmlKeywords (v_0)
+import Control.Arrow
+import Control.Arrow.ArrowList
+import Control.Arrow.ArrowTree
+
+atTag tag = deep (isElem >>> hasName tag)
+
+getTerm = getVar <+> getFunApp
+
+getVar = proc x -> do
+    nm <- getText <<< getChildren <<< hasName "var" -< x
+    returnA -< Var $ mk 0 nm
+
+getFunApp = proc x -> do
+    sub <- hasName "funapp" -< x
+    nm <- getText <<< gotoChild "name" -< sub
+    gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub
+    let c = mk (length gs) nm
+    returnA -< Node c gs
+          
+gotoChild tag = proc x -> do
+    returnA <<< getChildren <<< getChild tag -< x
+
+getChild tag = proc x -> do
+    returnA <<< hasName tag <<< isElem <<< getChildren -< x
+
+getProblem = atTag "problem" >>> proc x -> do
+    ty <- getType <<< getAttrValue "type" -< x
+    rs <- getTRS <<< getChild "trs" -< x
+    st <- getStrategy <<< getChild "strategy" -< x
+    stt <- listA ( getStartterm <<< getChild "startterm" ) -< x
+    returnA -< Problem { trs = rs
+                        , TPDB.Data.strategy = st
+                        , type_ = ty 
+                        , startterm = case stt of
+                             [] -> Nothing
+                             [x] -> x
+                        }
+
+getType = proc x -> do
+    returnA -< case x of
+        "termination" -> Termination
+        "complexity" -> Complexity
+
+getStrategy = proc x -> do
+    cs <- getText <<< getChildren -< x
+    returnA -< case cs of
+        "FULL" -> Just Full
+
+getStartterm = ( proc x -> do
+        getChild "constructor-based" -< x
+        returnA -< Just Startterm_Constructor_based
+   ) <+>  ( proc x -> do
+        getChild "full" -< x
+        returnA -< Just Startterm_Full
+   ) <+> ( proc x -> do returnA -< Nothing )
+
+getTRS = proc x -> do
+    sig <- getSignature <<< getChild "signature" -< x
+    str <- getRules Strict <<< getChild "rules" -< x
+    nostr <- listA ( getRules Weak <<< getChild "relrules" <<< getChild "rules" ) -< x
+    -- FIXME: check that symbols are use with correct arity
+    th <- listA ( atTag "theory" ) -< x
+    returnA -< case th of
+        [] -> RS { signature = sig
+                  , rules = str ++ concat nostr
+                  , separate = False -- for TRS, don't need comma between rules
+                  }
+        _  -> error $ unwords [ "cannot handle theories" ]
+
+getSignature = proc x -> do
+    returnA <<< listA ( getFuncsym <<< getChild "funcsym" ) -< x
+
+getFuncsym = proc x -> do
+    nm <- getText <<< gotoChild "name" -< x
+    ar <- getText <<< gotoChild "arity" -< x
+    returnA -< mk (read ar) nm
+
+getRules str = proc x -> do
+    returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x
+
+getRule str = proc x -> do
+    l <-  getTerm <<< isElem <<< gotoChild "lhs" -< x
+    r <-  getTerm <<< isElem <<< gotoChild "rhs" -< x
+    returnA -< Rule { lhs = l, relation = str, rhs = r, top = False }
+
+readProblems :: FilePath -> IO [ Problem Identifier Identifier ]
+readProblems file = do
+    cs <- readFile file
+    runX ( readString [] cs >>> getProblem )
+
+
+
diff --git a/src/TPDB/Xml.hs b/src/TPDB/Xml.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Xml.hs
@@ -0,0 +1,116 @@
+{-# language UndecidableInstances, OverlappingInstances, IncoherentInstances, FlexibleInstances, ScopedTypeVariables #-}
+
+module TPDB.Xml where
+
+import Text.XML.HaXml.Types (QName (..) )
+import Text.XML.HaXml.XmlContent.Haskell
+import Text.XML.HaXml.Posn ( Posn )
+
+import qualified Text.XML.HaXml.Pretty as P
+
+import Data.Typeable
+
+import Control.Monad
+import Control.Applicative
+       
+mkel name cs = CElem ( Elem (N name) [] cs ) ()
+rmkel name cs = return $ mkel name cs
+
+nospaceString :: String -> Content ()
+nospaceString s = CString False (escape s) ()
+
+instance Typeable t => HTypeable t where 
+    toHType x = let cs = show ( typeOf x ) in Prim cs cs
+
+escape [] = []
+escape ( c : cs ) = case c of
+    '<' -> "&lt;" ++ escape cs
+    '>' -> "&gt;" ++ escape cs
+    _   -> c :       escape cs
+
+
+type Contents = [ Content Posn ]
+
+data CParser a = CParser { unCParser :: Contents -> Maybe ( a, Contents ) }
+
+instance Functor CParser where
+    fmap f (CParser p) = CParser $ \ cs ->
+        do ( x, cs' ) <- p cs ; return ( f x, cs' )
+
+instance Applicative CParser where
+    pure = return ; (<*>) = ap
+         
+instance Monad CParser where
+    return x = CParser $ \ cs -> return ( x, cs )
+    CParser p >>= f = CParser $ \ cs0 -> 
+        do ( x, cs1 ) <- p cs0 ; unCParser ( must_succeed $ f x ) cs1
+
+
+must_succeed :: CParser a -> CParser a
+must_succeed (CParser p ) = CParser $ \ cs -> 
+    case p cs of
+        Nothing -> error $ "must succeed:" ++ errmsg cs
+	ok -> ok
+
+class Typeable a => XRead a where xread :: CParser a
+
+
+instance ( Typeable a, XmlContent a ) => XRead a where
+    xread = CParser $ \ cs -> case runParser parseContents cs of
+          ( Right x, rest ) -> Just ( x, rest )  
+          ( Left err, rest ) -> Nothing
+
+wrap :: forall a . Typeable a => CParser a -> Parser ( Content Posn ) a
+wrap ( CParser p ) = P $ \ cs -> case p cs of
+     Nothing -> Failure cs $ unlines
+	     $ "want expression of type " 
+	     :  show ( typeOf ( undefined :: a )) 
+	     :  errmsg cs
+	     : []
+     Just ( x, cs' ) -> Committed ( Success cs' x )
+
+errmsg cs = unlines $ case cs of 
+		  ( c  : etc ) -> 
+		     [ show $ P.content c
+		    
+		     ]
+		  _ -> [ show $ length cs ]
+
+orelse :: CParser a -> CParser a  -> CParser a
+orelse ( CParser p ) ( CParser q ) = CParser $ \ cs -> 
+    case p cs of Nothing -> q cs ; ok -> ok
+
+many :: CParser a -> CParser [a]
+many p = ( do x <- p ; xs <- TPDB.Xml.many p ; return $ x : xs ) `orelse` return []
+
+element tag p = element0 (N tag) $ must_succeed p
+
+element0 tag p = CParser $ \ cs -> case strip cs of
+     ( CElem ( Elem name atts con ) _ : etc ) | name == tag -> 
+         case unCParser p con of
+	     Nothing -> Nothing
+	     Just ( x, _ ) -> Just ( x, etc )
+     _ -> Nothing
+
+strip [] = []
+strip input @ ( CElem ( Elem {} ) _ : _ ) = input
+strip (c : cs) = strip cs
+
+xfromstring :: Read a => CParser a
+xfromstring = CParser $ \ cs -> case cs of
+    ( CString _ s _ : etc ) -> Just ( read s, etc )
+    _ -> Nothing
+
+complain :: String -> CParser a
+complain tag = CParser $ \ cs -> error $ "ERROR: in branch for " ++ tag ++ errmsg cs
+
+info :: Contents -> String
+info [] = "empty contents"
+info ( c : cs ) = case c of
+    CElem ( Elem name atts con ) _ -> "CElem, name: " ++ show name
+    CString _ s _ -> "CString : " ++ s
+    CRef _ _ -> "CRef"
+    CMisc _ _ -> "CMisc"
+
+
+
diff --git a/src/TPDB/Xml/Pretty.hs b/src/TPDB/Xml/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Xml/Pretty.hs
@@ -0,0 +1,298 @@
+-- | original author: Malcolm Wallace, 
+-- license: LGPL
+-- http://hackage.haskell.org/packages/archive/HaXml/1.23.3/doc/html/Text-XML-HaXml-Pretty.html
+--
+-- modified by Johannes Waldmann
+-- to use a different pretty-printer back-end.
+--
+-- This is a pretty-printer for turning the internal representation
+--   of generic structured XML documents into the Doc type (which can
+--   later be rendered using Text.PrettyPrint.HughesPJ.render).
+--   Essentially there is one pp function for each type in
+--   Text.Xml.HaXml.Types, so you can pretty-print as much or as little
+--   of the document as you wish.
+
+{-# language OverloadedStrings #-}
+
+module TPDB.Xml.Pretty
+  (
+  -- * Pretty-print a whole document
+    document
+  -- ** Just one content
+  ,   content
+  -- ** Just one tagged element
+  ,   element
+  -- * Pretty-print just a DTD
+  , doctypedecl
+  -- ** The prolog
+  ,   prolog
+  -- ** A content particle description
+  ,   cp
+  ) where
+
+import Prelude hiding (maybe,either)
+import Data.Maybe hiding (maybe)
+import Data.List (intersperse)
+--import Char (isSpace)
+
+-- import Text.PrettyPrint.HughesPJ
+import TPDB.Pretty hiding ( text )
+
+import Text.XML.HaXml.Types
+import Text.XML.HaXml.Namespaces
+
+import Data.String ( fromString )
+
+text = fromString
+
+either :: (t -> t1) -> (t2 -> t1) -> Either t t2 -> t1
+either f _ (Left x)  = f x
+either _ g (Right x) = g x
+
+maybe :: (t -> Doc) -> Maybe t -> Doc
+maybe _ Nothing  = empty
+maybe f (Just x) = f x
+
+--peref p   = "%" <> text p <> ";"
+
+----
+
+document :: Document i -> Doc
+prolog   :: Prolog -> Doc
+xmldecl  :: XMLDecl -> Doc
+misc     :: Misc -> Doc
+sddecl   :: Bool -> Doc
+
+doctypedecl :: DocTypeDecl -> Doc
+markupdecl  :: MarkupDecl -> Doc
+--extsubset   :: ExtSubset -> Doc
+--extsubsetdecl :: ExtSubsetDecl -> Doc
+cp          :: CP -> Doc
+
+element   :: Element i -> Doc
+attribute :: Attribute -> Doc                     --etc
+content   :: Content i -> Doc
+
+----
+
+document (Document p _ e m)= prolog p $$ element e $$ vcat (map misc m)
+prolog (Prolog x m1 dtd m2)= maybe xmldecl x $$
+                             vcat (map misc m1) $$
+                             maybe doctypedecl dtd $$
+                             vcat (map misc m2)
+xmldecl (XMLDecl v e sd)   = "<?xml version='" <> text v <> "'" <+>
+                             maybe encodingdecl e <+>
+                             maybe sddecl sd <+>
+                             "?>"
+misc (Comment s)           = "<!--" <> text s <> "-->"
+misc (PI (n,s))            = "<?" <> text n <+> text s <> "?>"
+sddecl sd   | sd           = "standalone='yes'"
+            | otherwise    = "standalone='no'"
+doctypedecl (DTD n eid ds) = if null ds then
+                                  hd <> ">"
+                             else hd <+> " [" $$
+                                  vcat (map markupdecl ds) $$ "]>"
+                           where hd = "<!DOCTYPE" <+> qname n <+>
+                                      maybe externalid eid
+markupdecl (Element e)     = elementdecl e
+markupdecl (AttList a)     = attlistdecl a
+markupdecl (Entity e)      = entitydecl e
+markupdecl (Notation n)    = notationdecl n
+markupdecl (MarkupMisc m)  = misc m
+--markupdecl (MarkupPE p m)  = peref p
+
+--extsubset (ExtSubset t ds) = maybe textdecl t $$
+--                             vcat (map extsubsetdecl ds)
+--extmarkupdecl (ExtMarkupDecl m)      = markupdecl m
+--extsubsetdecl (ExtConditionalSect c) = conditionalsect c
+-- -- extsubsetdecl (ExtPEReference p e)   = peref p
+
+element (Elem n as []) = "<" <> qname n <+>
+                         fsep (map attribute as) <> "/>"
+element e@(Elem n as cs)
+    | all isText cs    = "<" <> qname n <+> fsep (map attribute as) <>
+                         ">" <> hcat (map content cs) <>
+                         "</" <> qname n <> ">"
+    | otherwise        = let (d,c) = carryelem e empty
+                         in d <> c
+
+isText :: Content t -> Bool
+isText (CString _ _ _) = True
+isText (CRef _ _)      = True
+isText _               = False
+
+carryelem    ::  Element t  -> Doc -> (Doc, Doc)
+carrycontent ::  Content t  -> Doc -> (Doc, Doc)
+spancontent  :: [Content a] -> Doc -> ([Doc],Doc)
+
+carryelem (Elem n as []) c = ( c <>
+                               "<" <> qname n <+> fsep (map attribute as)
+                             , "/>")
+carryelem (Elem n as cs) c =  let (cs0,d0) = spancontent cs (">") in
+                              ( c <>
+                                "<"<>qname n <+> fsep (map attribute as) $$
+                                nest 2 (vcat cs0) <>
+                                d0 <> "</" <> qname n
+                              , ">")
+
+carrycontent (CElem e _) c         = carryelem e c
+carrycontent (CString False s _) c = (c <> chardata s, empty)
+carrycontent (CString True  s _) c = (c <> cdsect s, empty)
+carrycontent (CRef r _) c          = (c <> reference r, empty)
+carrycontent (CMisc m _) c         = (c <> misc m, empty)
+
+spancontent []     c = ([],c)
+spancontent (a:as) c | isText a  = let (ts,rest) = span isText (a:as)
+                                       formatted = c <> hcat (map content ts)
+                                   in  spancontent rest formatted
+                     | otherwise = let (b, c0) = carrycontent a c
+                                       (bs,c1) = spancontent as c0
+                                   in  (b:bs, c1)
+
+attribute (n,v)             = qname n <> "=" <> attvalue v
+content (CElem e _)         = element e
+content (CString False s _) = chardata s
+content (CString True s _)  = cdsect s
+content (CRef r _)          = reference r
+content (CMisc m _)         = misc m
+
+elementdecl :: ElementDecl -> Doc
+elementdecl (ElementDecl n cs) = "<!ELEMENT" <+> qname n <+>
+                                 contentspec cs <> ">"
+contentspec :: ContentSpec -> Doc
+contentspec EMPTY              = "EMPTY"
+contentspec ANY                = "ANY"
+contentspec (Mixed m)          = mixed m
+contentspec (ContentSpec c)    = cp c
+--contentspec (ContentPE p cs)   = peref p
+cp (TagName n m)       = parens (qname n) <> modifier m
+cp (Choice cs m)       = parens (hcat (intersperse ("|") (map cp cs))) <>
+                           modifier m
+cp (Seq cs m)          = parens (hcat (intersperse (",") (map cp cs))) <>
+                           modifier m
+--cp (CPPE p c)          = peref p
+modifier :: Modifier -> Doc
+modifier None          = empty
+modifier Query         = "?"
+modifier Star          = "*"
+modifier Plus          = "+"
+mixed :: Mixed -> Doc
+mixed  PCDATA          = "(#PCDATA)"
+mixed (PCDATAplus ns)  = "(#PCDATA |" <+>
+                         hcat (intersperse ("|") (map qname ns)) <>
+                         ")*"
+
+attlistdecl :: AttListDecl -> Doc
+attlistdecl (AttListDecl n ds) = "<!ATTLIST" <+> qname n <+>
+                                 fsep (map attdef ds) <> ">"
+attdef :: AttDef -> Doc
+attdef (AttDef n t d)          = qname n <+> atttype t <+> defaultdecl d
+atttype :: AttType -> Doc
+atttype  StringType            = "CDATA"
+atttype (TokenizedType t)      = tokenizedtype t
+atttype (EnumeratedType t)     = enumeratedtype t
+tokenizedtype :: TokenizedType -> Doc
+tokenizedtype ID               = "ID"
+tokenizedtype IDREF            = "IDREF"
+tokenizedtype IDREFS           = "IDREFS"
+tokenizedtype ENTITY           = "ENTITY"
+tokenizedtype ENTITIES         = "ENTITIES"
+tokenizedtype NMTOKEN          = "NMTOKEN"
+tokenizedtype NMTOKENS         = "NMTOKENS"
+enumeratedtype :: EnumeratedType -> Doc
+enumeratedtype (NotationType n)= notationtype n
+enumeratedtype (Enumeration e) = enumeration e
+notationtype :: [String] -> Doc
+notationtype ns                = "NOTATION" <+>
+                                 parens (hcat (intersperse ("|") (map text ns)))
+enumeration :: [String] -> Doc
+enumeration ns                 = parens (hcat (intersperse ("|") (map nmtoken ns)))
+defaultdecl :: DefaultDecl -> Doc
+defaultdecl  REQUIRED          = "#REQUIRED"
+defaultdecl  IMPLIED           = "#IMPLIED"
+defaultdecl (DefaultTo a f)    = maybe (const ("#FIXED")) f <+> attvalue a
+--conditionalsect (IncludeSect i)= "<![INCLUDE [" <+>
+--                                 vcat (map extsubsetdecl i) <+> "]]>"
+--conditionalsect (IgnoreSect i) = "<![IGNORE [" <+>
+--                                 fsep (map ignoresectcontents i) <+> "]]>"
+--ignore (Ignore)                = empty
+--ignoresectcontents (IgnoreSectContents i is)
+--                               = ignore i <+> vcat (map internal is)
+--                          where internal (ics,i) = "<![[" <+>
+--                                                   ignoresectcontents ics <+>
+--                                                   "]]>" <+> ignore i
+reference :: Reference -> Doc
+reference (RefEntity er)       = entityref er
+reference (RefChar cr)         = charref cr
+entityref :: String -> Doc
+entityref n                    = "&" <> text n <> ";"
+charref :: (Show a) => a -> Doc
+charref c                      = "&#" <> text (show c) <> ";"
+entitydecl :: EntityDecl -> Doc
+entitydecl (EntityGEDecl d)    = gedecl d
+entitydecl (EntityPEDecl d)    = pedecl d
+gedecl :: GEDecl -> Doc
+gedecl (GEDecl n ed)           = "<!ENTITY" <+> text n <+> entitydef ed <>
+                                 ">"
+pedecl :: PEDecl -> Doc
+pedecl (PEDecl n pd)           = "<!ENTITY %" <+> text n <+> pedef pd <>
+                                 ">"
+entitydef :: EntityDef -> Doc
+entitydef (DefEntityValue ew)  = entityvalue ew
+entitydef (DefExternalID i nd) = externalid i <+> maybe ndatadecl nd
+pedef :: PEDef -> Doc
+pedef (PEDefEntityValue ew)    = entityvalue ew
+pedef (PEDefExternalID eid)    = externalid eid
+externalid :: ExternalID -> Doc
+externalid (SYSTEM sl)         = "SYSTEM" <+> systemliteral sl
+externalid (PUBLIC i sl)       = "PUBLIC" <+> pubidliteral i <+>
+                                 systemliteral sl
+ndatadecl :: NDataDecl -> Doc
+ndatadecl (NDATA n)            = "NDATA" <+> text n
+--textdecl (TextDecl vi ed)      = "<?xml" <+> maybe text vi <+>
+--                                 encodingdecl ed <+> "?>"
+--extparsedent (ExtParsedEnt t c)= maybe textdecl t <+> content c
+--extpe (ExtPE t esd)            = maybe textdecl t <+>
+--                                 vcat (map extsubsetdecl esd)
+notationdecl :: NotationDecl -> Doc
+notationdecl (NOTATION n e)    = "<!NOTATION" <+> text n <+>
+                                 either externalid publicid e <>
+                                 ">"
+publicid :: PublicID -> Doc
+publicid (PUBLICID p)          = "PUBLIC" <+> pubidliteral p
+encodingdecl :: EncodingDecl -> Doc
+encodingdecl (EncodingDecl s)  = "encoding='" <> text s <> "'"
+nmtoken :: String -> Doc
+nmtoken s                      = text s
+attvalue :: AttValue -> Doc
+attvalue (AttValue esr)        = "\"" <>
+                                 hcat (map (either text reference) esr) <>
+                                 "\""
+entityvalue :: EntityValue -> Doc
+entityvalue (EntityValue evs)
+  | containsDoubleQuote evs    = "'"  <> hcat (map ev evs) <> "'"
+  | otherwise                  = "\"" <> hcat (map ev evs) <> "\""
+ev :: EV -> Doc
+ev (EVString s)                = text s
+--ev (EVPERef p e)               = peref p
+ev (EVRef r)                   = reference r
+pubidliteral :: PubidLiteral -> Doc
+pubidliteral (PubidLiteral s)
+    | '"' `elem` s             = "'" <> text s <> "'"
+    | otherwise                = "\"" <> text s <> "\""
+systemliteral :: SystemLiteral -> Doc
+systemliteral (SystemLiteral s)
+    | '"' `elem` s             = "'" <> text s <> "'"
+    | otherwise                = "\"" <> text s <> "\""
+chardata :: String -> Doc
+chardata s                     = {-if all isSpace s then empty else-} text s
+cdsect :: String -> Doc
+cdsect c                       = "<![CDATA[" <> chardata c <> "]]>"
+
+qname n                        = text (printableName n)
+
+----
+containsDoubleQuote :: [EV] -> Bool
+containsDoubleQuote evs = any csq evs
+    where csq (EVString s) = '"' `elem` s
+          csq _            = False
diff --git a/test/speed.hs b/test/speed.hs
--- a/test/speed.hs
+++ b/test/speed.hs
@@ -32,9 +32,13 @@
         [ CElem e _ ] =  l
     in  Document pro emptyST e []
 
-main = do
-    -- print $ P.document
-    -- putStrLn $ renderStyle (Style LeftMode undefined undefined ) $ P.document
-    -- BS.putStrLn $ BSP.document
+main =  do
+    -- print $ P.document $ double 132
+
+    let s = (Style LeftMode undefined undefined )    
+    -- putStrLn $ renderStyle s $ P.document $ double 132
+
+    -- BS.putStrLn $ BSP.document $ double 132
+
     TP.displayIO stdout $ TP.renderCompact $ TXP.document
             $  double 132
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
 Name: tpdb
-Version: 1.1.1
+Version: 1.2.0
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Logic
@@ -28,9 +28,9 @@
 --   test/3.15.xml, test/33.trs ,  test/z001.srs
 
 Library
-  Build-Depends: base==4.*, hxt, wl-pprint-text, mtl,
+  Build-Depends: base==4.*, hxt, wl-pprint-text, text, mtl,
     parsec, time, containers, HaXml, filepath, hashable
-
+  Hs-Source-Dirs: src
   Exposed-Modules:
     TPDB.Data,     TPDB.Data.Term, TPDB.Data.Xml
     -- TPDB.Compress, 
@@ -50,31 +50,31 @@
 --    Build-depends: base==4.*, containers >= 0.5, directory, wl-pprint-text, hxt, parsec, hashable
 
 Test-Suite XML
-  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable
+  Build-Depends: base==4.*, tpdb
   Type: exitcode-stdio-1.0
   main-is: read_print_xml.hs
-  hs-source-dirs: test .
+  hs-source-dirs: test 
 
 Test-Suite TRS
-  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable
+  Build-Depends: base==4.*, tpdb
   Type: exitcode-stdio-1.0
   main-is: read_print_trs.hs
-  hs-source-dirs: test .
+  hs-source-dirs: test 
 
 Test-Suite TRS_02
-  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable
+  Build-Depends: base==4.*, tpdb
   Type: exitcode-stdio-1.0
   main-is: read_print_trs_2.hs
-  hs-source-dirs: test .
+  hs-source-dirs: test 
 
 Test-Suite SRS
-  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable
+  Build-Depends: base==4.*, tpdb
   Type: exitcode-stdio-1.0
   main-is: read_print_srs.hs
-  hs-source-dirs: test .
+  hs-source-dirs: test 
 
 Test-Suite Speed
-  Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers  >= 0.5, HaXml, hashable, pretty,bytestring
+  Build-Depends: base==4.*, tpdb, HaXml, bytestring, pretty
   Type: exitcode-stdio-1.0
   main-is: speed.hs
-  hs-source-dirs: test .
+  hs-source-dirs: test