packages feed

tpdb (empty) → 0.0

raw patch · 11 files changed

+399/−0 lines, 11 filesdep +basedep +hxtdep +parsecsetup-changed

Dependencies added: base, hxt, parsec, pretty

Files

+ LICENSE view
@@ -0,0 +1,1 @@+GPL
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ TPDB/Data.hs view
@@ -0,0 +1,39 @@+module TPDB.Data where++data Identifier = Identifier { name :: String , arity :: Int }+    deriving ( Eq, Ord, Show )++data Term v s = Var v +              | Node s [ Term v s ]+    deriving Show++data Rule a = Rule { lhs :: a, rhs :: a +                   , strict :: Bool+                   , top :: Bool+                   }+    deriving Show++data RS s r = +     RS { signature :: [ s ] -- ^ better keep order in signature (?)+         , rules :: [ Rule r ]+        , separate :: Bool -- ^ if True, write comma between rules+         }+    deriving Show++type TRS v s = RS s ( Term v s )++type SRS s = RS s [ s ]++data Problem v s = +     Problem { trs :: TRS v s+             , strategy :: Strategy+             -- , metainformation :: Metainformation+             , type_ :: Type +             }+     deriving Show++data Type = Termination | Complexity+     deriving Show ++data Strategy = Full | Innermost | Outermost+     deriving Show
+ TPDB/Plain/Read.hs view
@@ -0,0 +1,123 @@+-- | 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 Control.Monad ( guard, void )+++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 $ Identifier { arity = 0, name = 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 s ) => Reader ( Term v s ) where+    reader = do+        f  <- reader +        xs <- option [] $ parens lexer $ commaSep lexer reader+        return $ Node f xs++instance Reader u => Reader ( Rule u ) where+    reader = do+        l <- reader+        s <-  do reservedOp lexer "->"  ; return True+          <|> do reservedOp lexer "->=" ; return False+        r <- reader+        return $ Rule { lhs = l, strict = s, 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 commaSep lexer 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+        ds <- many $ declaration True+	return $ make_srs ds++instance Reader ( TRS Identifier Identifier ) where+    reader = do+        ds <- many $ declaration False+	return $ make_trs ds++make_srs :: [ Declaration [s] ] -> SRS s+make_srs ds = +    let us = do Rules_Declaration us <- ds ; us+    in  RS { signature = [] , rules = us, separate = True }++make_trs :: [ Declaration ( Term Identifier Identifier ) ] +         -> TRS Identifier Identifier+make_trs ds =+    let vs = do Var_Declaration vs <- ds ; vs+        us = do Rules_Declaration us <- ds ; us+        us' = repair_variables vs us+    in  RS { signature = [], 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 view
@@ -0,0 +1,44 @@+-- | the "old" TPDB format +-- cf. <http://www.lri.fr/~marche/tpdb/format.html>++{-# language FlexibleContexts #-}++module TPDB.Plain.Write where++import TPDB.Data++import Text.PrettyPrint.HughesPJ++class Pretty a where pretty :: a -> Doc++instance Pretty Identifier where+    pretty i = text $ 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 Pretty a => Pretty ( Rule a ) where+    pretty u = hsep [ pretty $ lhs u+                    , if strict u then text "->" else text "->="+                    -- FIXME: implement "top" annotation+                    , pretty $ rhs u+                    ]++instance Pretty s => Pretty [s] where+    pretty xs = hsep $ map pretty xs++instance ( Pretty s, Pretty r ) => Pretty ( RS s r ) where+    pretty sys = vcat +        [ parens $ text "RULES" <+>+          vcat ( ( if separate sys then punctuate comma else id )+                 $ map pretty $ rules sys +               )+        -- FIXME: output strategy, theory+        ]++instance ( Pretty s, Pretty r ) => Pretty ( Problem s r ) where+    pretty p = pretty $ trs p
+ 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+
+ TPDB/XTC/Read.hs view
@@ -0,0 +1,99 @@+{-# 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 $ Identifier { arity = 0, name = nm }++getFunApp = proc x -> do+    sub <- hasName "funapp" -< x+    nm <- getText <<< gotoChild "name" -< sub+    gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub+    let c = Identifier { arity = length gs , name = 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+    returnA -< case st of+        Full -> Problem { trs = rs+                        , TPDB.Data.strategy = st+                        , type_ = ty +                        }+        _    -> error $ unwords [ "cannot handle strategy", show st ]++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" -> Full++getTRS = proc x -> do+    sig <- getSignature <<< getChild "signature" -< x+    str <- getRules True <<< getChild "rules" -< x+    nostr <- listA ( getRules False <<< 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 -< Identifier { arity = read ar, name = 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, strict = str, rhs = r, top = False }++readProblems :: FilePath -> IO [ Problem Identifier Identifier ]+readProblems file = do+    cs <- readFile file+    runX ( readString [] cs >>> getProblem )+++
+ test/read_print_srs.hs view
@@ -0,0 +1,10 @@+import TPDB.Plain.Write+import TPDB.Plain.Read++import Control.Monad ( forM, void )++main = void $ do+    s <- readFile "test/z001.srs"+    case srs s of+        Right t -> print $ pretty t+        Left err -> error err
+ test/read_print_trs.hs view
@@ -0,0 +1,10 @@+import TPDB.Plain.Write+import TPDB.Plain.Read++import Control.Monad ( forM, void )++main = void $ do+    s <- readFile "test/33.trs"+    case trs s of+        Right t -> print $ pretty t+        Left err -> error err
+ test/read_print_xml.hs view
@@ -0,0 +1,12 @@++import TPDB.Data++import TPDB.XTC+import TPDB.Plain.Write++import Control.Monad ( forM, void )++main = void $ do+    ps <- readProblems "test/3.15.xml"+    print $ length ps+    forM ps ( print . pretty )
+ tpdb.cabal view
@@ -0,0 +1,47 @@+Name: tpdb+Version: 0.0+Author: Johannes Waldmann+Maintainer: Johannes Waldmann+Category: Science+License: GPL+License-file: LICENSE+Cabal-Version: >= 1.8+Synopsis: Data Type for Rewriting Systems+++Description:+   The package defines data types and parsers for rewriting systems,+   as used in the Termination Competitions.+   For syntax and semantics specification, +   see <http://www.termination-portal.org/wiki/TPDB>++Build-Type: Simple++Source-Repository head+  Type: git+  Location: git://dfa.imn.htwk-leipzig.de/srv/git/tpdb/++Library+  Build-Depends: base==4.*, hxt, pretty, parsec++  Exposed-Modules:+    TPDB.Data, +    TPDB.Plain.Write,     TPDB.Plain.Read,+    TPDB.XTC,  TPDB.XTC.Read++Test-Suite XML+  Type: exitcode-stdio-1.0+  main-is: read_print_xml.hs+  hs-source-dirs: test .++Test-Suite TRS+  Type: exitcode-stdio-1.0+  main-is: read_print_trs.hs+  hs-source-dirs: test .++Test-Suite SRS+  Type: exitcode-stdio-1.0+  main-is: read_print_srs.hs+  hs-source-dirs: test .++