packages feed

tpdb 1.1.1 → 1.2.0

raw patch · 50 files changed

+2277/−2267 lines, 50 filesdep +textdep +tpdbdep ~containers

Dependencies added: text, tpdb

Dependency ranges changed: containers

Files

− TPDB/CPF/Proof/Read.hs 
@@ -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---
− TPDB/CPF/Proof/Type.hs 
@@ -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 )
− TPDB/CPF/Proof/Util.hs 
@@ -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"
− TPDB/CPF/Proof/Write.hs 
@@ -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-    ]
− TPDB/CPF/Proof/Xml.hs 
@@ -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
− TPDB/Convert.hs 
@@ -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 )
− TPDB/DP.hs 
@@ -1,7 +0,0 @@-module TPDB.DP ( module TPDB.DP.Transform )--where--import TPDB.DP.Transform-import TPDB.DP.Graph-
− TPDB/DP/Graph.hs 
@@ -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)))"-
− TPDB/DP/TCap.hs 
@@ -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 -
− TPDB/DP/Transform.hs 
@@ -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 -         }
− TPDB/DP/Unify.hs 
@@ -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-
− TPDB/DP/Usable.hs 
@@ -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 -> []-
− TPDB/Data.hs 
@@ -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 }--
− TPDB/Data/Term.hs 
@@ -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
− TPDB/Data/Xml.hs 
@@ -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-               ]---
− TPDB/Input.hs 
@@ -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-            -
− TPDB/Mirror.hs 
@@ -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 }
− TPDB/Plain/Read.hs 
@@ -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-		  }-
− TPDB/Plain/Write.hs 
@@ -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 ) ] -       ]
− TPDB/Pretty.hs 
@@ -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)
− TPDB/XTC.hs 
@@ -1,12 +0,0 @@-module TPDB.XTC --( module TPDB.Data-, module TPDB.XTC.Read-)---where--import TPDB.Data-import TPDB.XTC.Read-
− TPDB/XTC/Read.hs 
@@ -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 )---
− TPDB/Xml.hs 
@@ -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"---
− TPDB/Xml/Pretty.hs 
@@ -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
+ src/TPDB/CPF/Proof/Read.hs view
@@ -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+++
+ src/TPDB/CPF/Proof/Type.hs view
@@ -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 )
+ src/TPDB/CPF/Proof/Util.hs view
@@ -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"
+ src/TPDB/CPF/Proof/Write.hs view
@@ -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+    ]
+ src/TPDB/CPF/Proof/Xml.hs view
@@ -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
+ src/TPDB/Convert.hs view
@@ -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 )
+ src/TPDB/DP.hs view
@@ -0,0 +1,7 @@+module TPDB.DP ( module TPDB.DP.Transform )++where++import TPDB.DP.Transform+import TPDB.DP.Graph+
+ src/TPDB/DP/Graph.hs view
@@ -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)))"+
+ src/TPDB/DP/TCap.hs view
@@ -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 +
+ src/TPDB/DP/Transform.hs view
@@ -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 +         }
+ src/TPDB/DP/Unify.hs view
@@ -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+
+ src/TPDB/DP/Usable.hs view
@@ -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 -> []+
+ src/TPDB/Data.hs view
@@ -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 }++
+ src/TPDB/Data/Term.hs view
@@ -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
+ src/TPDB/Data/Xml.hs view
@@ -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+               ]+++
+ src/TPDB/Input.hs view
@@ -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+            +
+ src/TPDB/Mirror.hs view
@@ -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 }
+ src/TPDB/Plain/Read.hs view
@@ -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+		  }+
+ src/TPDB/Plain/Write.hs view
@@ -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 ) ] +       ]
+ src/TPDB/Pretty.hs view
@@ -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)
+ src/TPDB/XTC.hs view
@@ -0,0 +1,12 @@+module TPDB.XTC ++( module TPDB.Data+, module TPDB.XTC.Read+)+++where++import TPDB.Data+import TPDB.XTC.Read+
+ src/TPDB/XTC/Read.hs view
@@ -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 )+++
+ src/TPDB/Xml.hs view
@@ -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"+++
+ src/TPDB/Xml/Pretty.hs view
@@ -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
test/speed.hs view
@@ -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
tpdb.cabal view
@@ -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