tpdb 2.8.6 → 2.9.0
raw patch · 6 files changed
+136/−14 lines, 6 filesdep +atto-lispdep +attoparsecdep +unordered-containersdep ~prettyprinter
Dependencies added: atto-lisp, attoparsec, unordered-containers
Dependency ranges changed: prettyprinter
Files
- src/TPDB/ARI.hs +93/−0
- src/TPDB/Input/File.hs +14/−4
- src/TPDB/Input/Memory.hs +2/−1
- src/TPDB/Pretty.hs +0/−3
- test/read_ARI.hs +12/−0
- tpdb.cabal +15/−6
+ src/TPDB/ARI.hs view
@@ -0,0 +1,93 @@+{-# language OverloadedStrings #-}+{- # options_ghc -fdefer-typed-holes #-}++module TPDB.ARI where++import Data.AttoLisp+import qualified Data.Attoparsec.ByteString as DAB+import Data.Attoparsec.Number+import qualified Data.ByteString as BS+import qualified Data.ByteString.Lazy as BSL+import qualified Data.Text as T+import qualified Data.HashMap.Strict as M+import Control.Applicative (many)+import Control.Monad (guard)+import TPDB.Data+import TPDB.Plain.Write+import TPDB.Pretty++-- writer+put :: TRS Identifier Identifier -> BSL.ByteString+put = BSL.concat . map encodeLn . w++encodeLn x = encode x `BSL.snoc` lf+ where lf = fromIntegral $ fromEnum '\n' -- HACK++w :: TRS Identifier Identifier -> [Lisp]+w sys =+ let sym s = Symbol $ name s+ sig = do+ s <- signature sys+ return $ List [ Symbol "fun", sym s+ , Number $ I $ fromIntegral $ arity s+ ]+ trm t = case t of+ Var v -> sym v+ Node f args -> List $ sym f : map trm args+ rul = do+ u <- rules sys+ return $ List+ $ [ Symbol "rule", trm (lhs u), trm (rhs u) ]+ <> case relation u of+ Strict -> []+ Weak -> [ Symbol ":cost", Number (I 0) ]+ in [ List [Symbol "format", Symbol "TRS" ] ]+ <> sig+ <> rul+++-- parser++get :: BS.ByteString -> Either String (TRS Identifier Identifier)+get s = DAB.parseOnly ( p <* DAB.atEnd ) s++p :: DAB.Parser (TRS Identifier Identifier)+p = do+ cl : auses <- many lisp+ guard $ cl == List [Symbol "format", Symbol "TRS"]+ let symbolize s0 = maybe s0 id $ do+ ('|', s1) <- T.uncons s0; (s2, '|') <- T.unsnoc s1; return s2+ funs = do+ List [Symbol "fun", Symbol s, Number (I a)] <- auses+ return (s, mk (fromIntegral a) $ symbolize s)+ sig = M.fromListWith (error "conflict") funs+ let rs :: [ Rule (Term Identifier Identifier) ]+ rs = do+ List (Symbol "rule" : l : r : trailer) <- auses+ return $ Rule { lhs = termof sig l+ , rhs = termof sig r+ , relation = case trailer of+ [ ] -> Strict+ [ Symbol ":cost", Number (I 0) ]+ -> Weak+ , top = False+ , original_variable = Nothing+ }+ return $ RS+ { signature = map snd funs+ , rules = rs+ , separate = False+ }++termof :: M.HashMap T.Text Identifier -> Lisp+ -> Term Identifier Identifier+termof sig (List (Symbol s : args)) =+ case M.lookup s sig of+ Just f | arity f == length args ->+ Node f $ map (termof sig) args+termof sig (Symbol s) = case M.lookup s sig of+ Nothing -> Var $ mk 0 s+ Just f -> Node f [] -- ?+ + +
src/TPDB/Input/File.hs view
@@ -2,15 +2,17 @@ import TPDB.Data import TPDB.Convert+import qualified TPDB.ARI import qualified TPDB.Input.Memory as TIM import qualified Data.Text.Lazy as T import qualified Data.Text.Lazy.IO as T+import qualified Data.ByteString as BS import System.FilePath.Posix ( takeExtension ) -- | read input from file with given name.--- can have extension .srs, .trs, .xml.+-- can have extension .srs, .trs, .xml, .ari -- unknown extension is considered as .xml, because of -- http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks @@ -23,9 +25,17 @@ Right x -> return x Left err -> error err -getE f = do- s <- T.readFile f- TIM.get f s+getE :: FilePath + -> IO (Either String+ ( Either (TRS Identifier Identifier) + ( SRS Identifier ) ) )+getE f = case takeExtension f of+ ".ari" -> do+ s <- BS.readFile f+ return $ fmap Left $ TPDB.ARI.get s+ _ -> do+ s <- T.readFile f+ TIM.get f s get_trs f = do x <- get f
src/TPDB/Input/Memory.hs view
@@ -7,12 +7,13 @@ import TPDB.Data import TPDB.Plain.Read import TPDB.XTC.Read+import qualified TPDB.ARI import qualified Data.Text.Lazy as T import System.FilePath.Posix ( takeExtension ) -- | first argument is file name, second argument is file contents.--- first arg. is needed to pick the proper parser (SRS, TRS, XTC)+-- first arg. is needed to pick the proper parser (SRS, TRS, XTC, ARI) get :: String -> T.Text -> IO (Either String (Either (TRS Identifier Identifier) (SRS Identifier))) get f s = case takeExtension f of
src/TPDB/Pretty.hs view
@@ -53,9 +53,6 @@ text :: String -> D.Doc ann text = fromString -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 ]- -- | WARNING: there is instance Pretty a => Pretty (Maybe a) in the back-end -- but its spec is "Ignore Nothings, print Just contents"
+ test/read_ARI.hs view
@@ -0,0 +1,12 @@+import TPDB.Data+import TPDB.Pretty+import TPDB.Input.File+import TPDB.Plain.Write++import Control.Monad ( forM, void )++main = void $ do+ p <- get_trs "test/01.ari"+ print $ pretty p++
tpdb.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 3.8 Name: tpdb-Version: 2.8.6+Version: 2.9.0 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann@@ -20,19 +20,20 @@ Homepage: https://github.com/jwaldmann/haskell-tpdb -tested-with: GHC == 9.12.2+tested-with: GHC == 9.12.2, GHC == 9.14.1 Extra-Source-Files: test/*.xml, test/*.trs , test/*.srs, test/*.cpf Source-Repository head Type: git- Location: git://github.com/jwaldmann/haskell-tpdb.git+ Location: https://github.com/jwaldmann/haskell-tpdb Library- Build-Depends: base==4.*, prettyprinter, text, mtl,+ Build-Depends: base==4.*, prettyprinter >= 1.7.2, text, mtl, xml-hamlet, xml-conduit, data-default,- parsec, time, containers, filepath, hashable, bytestring, exceptions+ parsec, time, containers, filepath, hashable, bytestring, exceptions,+ attoparsec,atto-lisp,unordered-containers Hs-Source-Dirs: src default-language: Haskell2010 Exposed-Modules:@@ -47,7 +48,8 @@ TPDB.XTC, TPDB.XTC.Read, TPDB.XTC.Write, TPDB.Xml, TPDB.CPF.Proof.Write, TPDB.CPF.Proof.Read, TPDB.CPF.Proof.Xml, - TPDB.CPF.Proof.Type, TPDB.CPF.Proof.Util+ TPDB.CPF.Proof.Type, TPDB.CPF.Proof.Util,+ TPDB.ARI Executable plain2xtc build-depends: base==4.*, tpdb, bytestring@@ -150,6 +152,13 @@ Build-Depends: base==4.*, tpdb Type: exitcode-stdio-1.0 main-is: read_complex.hs+ hs-source-dirs: test + default-language: Haskell2010++Test-Suite read-ARI+ Build-Depends: base==4.*, tpdb+ Type: exitcode-stdio-1.0+ main-is: read_ARI.hs hs-source-dirs: test default-language: Haskell2010