tpdb 1.3.3 → 1.5.2
raw patch · 15 files changed
+263/−67 lines, 15 filesdep +data-defaultdep +prettyprinterdep +xml-conduitdep −wl-pprint-textnew-component:exe:plain2xtc
Dependencies added: data-default, prettyprinter, xml-conduit, xml-hamlet
Dependencies removed: wl-pprint-text
Files
- plain2xtc.hs +13/−0
- src/TPDB/CPF/Proof/Read.hs +18/−1
- src/TPDB/CPF/Proof/Type.hs +31/−2
- src/TPDB/Convert.hs +12/−10
- src/TPDB/Plain/Write.hs +3/−3
- src/TPDB/Pretty.hs +41/−40
- src/TPDB/XTC.hs +3/−0
- src/TPDB/XTC/Read.hs +7/−5
- src/TPDB/XTC/Write.hs +62/−0
- src/TPDB/Xml/Pretty.hs +4/−1
- test/parse_ac.hs +12/−0
- test/read_complex.hs +12/−0
- test/read_cpf.hs +10/−0
- test/read_print_trs.hs +2/−1
- tpdb.cabal +33/−4
+ plain2xtc.hs view
@@ -0,0 +1,13 @@+import qualified TPDB.Data as D+import qualified TPDB.Input as I+import qualified TPDB.XTC as X+import System.Environment (getArgs)+import qualified Data.ByteString.Lazy as L++main = do+ [f] <- getArgs+ s <- I.get_trs f+ L.putStrLn $ X.renderLBS X.def $ X.document+ $ D.Problem { D.type_ = D.Termination, D.trs = s+ , D.strategy = Just D.Full+ }
src/TPDB/CPF/Proof/Read.hs view
@@ -39,12 +39,28 @@ returnA -< CertificationProblem { input = inp, proof = pro, cpfVersion = ver, origin = ignoredOrigin } -getInput = getTerminationInput <+> getComplexityInput+getInput = getTerminationInput <+> getComplexityInput <+> getACTerminationInput getTerminationInput = hasName "input" >>> proc x -> do trsI <- getTrsInput <<< getChild "trsInput" -< x returnA -< TrsInput $ RS { rules = trsI, separate = False } +getACTerminationInput = hasName "input" >>> proc x -> do+ acrs <- getChild "acRewriteSystem" -< x+ trsI <- getTrsInput -< acrs+ as <- listA getSymbol <<< getChild "Asymbols" -< acrs+ cs <- listA getSymbol <<< getChild "Csymbols" -< acrs+ returnA -< ACRewriteSystem+ { trsinput_trs = RS { rules = trsI, separate = False }+ , asymbols = as+ , csymbols = cs+ }++getSymbol = proc x -> do+ s <- getText <<< gotoChild "name" -< x+ returnA -< mk 0 s++ getComplexityInput = hasName "input" >>> proc x -> do y <- getChild "complexityInput" -< x trsI <- getTrsInput <<< getChild "trsInput" -< y@@ -80,6 +96,7 @@ <+> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined ) <+> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined ) <+> getDummy "complexityProof" ( ComplexityProof undefined )+ <+> getDummy "acTerminationProof" ( ACTerminationProof undefined ) getDummy t c = proc x -> do getChild t -< x
src/TPDB/CPF/Proof/Type.hs view
@@ -1,6 +1,7 @@ {-# language StandaloneDeriving #-} {-# language ExistentialQuantification #-} {-# language DeriveDataTypeable #-}+{-# language OverloadedStrings #-} -- | internal representation of CPF termination proofs, -- see <http://cl-informatik.uibk.ac.at/software/cpf/>@@ -15,7 +16,9 @@ where import TPDB.Data+import TPDB.Plain.Write () import Data.Typeable+import TPDB.Pretty import Text.XML.HaXml.XmlContent.Haskell hiding ( text ) @@ -46,13 +49,35 @@ , complexityMeasure :: ComplexityMeasure , complexityClass :: ComplexityClass }+ | ACRewriteSystem { trsinput_trs :: TRS Identifier Identifier+ , asymbols :: [ Identifier ]+ , csymbols :: [ Identifier ]+ } deriving ( Typeable, Eq ) +instance Pretty CertificationProblemInput where+ pretty cpi = case cpi of+ TrsInput { } ->+ "TrsInput" <+> vcat [ "trs" <+> pretty (trsinput_trs cpi) ]+ ComplexityInput { } ->+ "ComplexityInput" <+> vcat+ [ "trs" <+> pretty (trsinput_trs cpi)+ , "measure" <+> text (show $ complexityMeasure cpi )+ , "class" <+> text (show $ complexityClass cpi )+ ]+ ACRewriteSystem { } ->+ "ACRewritesystem" <+> vcat+ [ "trs" <+> pretty (trsinput_trs cpi)+ , "asymbols" <+> text (show $ asymbols cpi )+ , "csymbols" <+> text (show $ csymbols cpi )+ ]+ data Proof = TrsTerminationProof TrsTerminationProof | TrsNonterminationProof TrsNonterminationProof | RelativeTerminationProof TrsTerminationProof | RelativeNonterminationProof TrsNonterminationProof | ComplexityProof ComplexityProof+ | ACTerminationProof ACTerminationProof deriving ( Typeable, Eq ) data DPS = forall s . ( XmlContent s , Typeable s, Eq s ) @@ -68,14 +93,14 @@ data ComplexityMeasure = DerivationalComplexity | RuntimeComplexity- deriving ( Typeable, Eq )+ deriving ( Typeable, Eq, Show ) 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 )+ deriving ( Typeable, Eq, Show ) data TrsNonterminationProof = TrsNonterminationProofFIXME () deriving ( Typeable, Eq )@@ -254,3 +279,7 @@ , afeFilter :: Either Int [Int] } deriving ( Typeable, Eq )++data ACTerminationProof = ACTerminationProofFIXME ()+ deriving ( Typeable, Eq )+
src/TPDB/Convert.hs view
@@ -6,25 +6,27 @@ srs2trs :: SRS Identifier -> TRS Identifier Identifier srs2trs s = s { separate = False , rules = map convert_srs_rule $ rules s- } + , signature = map (set_arity 1) $ signature s+ } -convert_srs_rule u = +set_arity a s = s { arity = a }++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 - } - + , rhs = handle $ rhs u+ }+ trs2srs :: Eq v => TRS v s -> Maybe ( SRS s ) trs2srs t = do- us <- forM ( rules t ) convert_trs_rule + 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 + guard $ left_base == right_base return $ u { lhs = left_spine, rhs = right_spine } unspine :: v -> [s] -> Term v s@@ -36,6 +38,6 @@ spine t = case t of Node f args -> do [ arg ] <- return args- ( sp, base ) <- spine arg + ( sp, base ) <- spine arg return ( f : sp, base )- Var v -> return ( [] , v ) + Var v -> return ( [] , v )
src/TPDB/Plain/Write.hs view
@@ -22,6 +22,9 @@ [] -> pretty f _ -> pretty f <+> ( parens $ fsep $ punctuate comma $ map pretty xs ) +class PrettyTerm a where + prettyTerm :: a -> Doc ann+ instance PrettyTerm a => Pretty ( Rule a ) where pretty u = sep [ prettyTerm $ lhs u , ( case relation u of @@ -31,9 +34,6 @@ -- 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
src/TPDB/Pretty.hs view
@@ -1,62 +1,63 @@-module TPDB.Pretty +{-# language NoMonomorphismRestriction #-} -( Doc, SimpleDoc-, render, renderCompact, displayIO-, Pretty (..)+module TPDB.Pretty++( Doc, Pretty (..)+, render, renderWide, renderCompact, renderPretty+, displayIO , fsep, sep, hsep, vsep, vcat, hcat , parens, brackets, angles, braces, enclose-, punctuate, comma, nest-, empty, text-, (<>), (<+>), ($$)+, encloseSep, punctuate, comma, nest, list, tupled+ , module Data.Monoid, empty+, text+, (<+>), ($$)+, indent, nest, hang ) where -import Text.PrettyPrint.Leijen.Text - hiding ( text, (<+>), vcat, hcat, vsep, hsep, sep, parens )-import qualified Text.PrettyPrint.Leijen.Text +import Data.Text.Prettyprint.Doc+ ( Doc, Pretty(..), comma+ , punctuate, encloseSep, align, parens, braces, angles, brackets, nest, enclose+ , list, tupled+ , indent, nest, hang+ )+import qualified Data.Text.Prettyprint.Doc as D+import qualified Data.Text.Prettyprint.Doc.Render.Text as T+ import Data.String ( fromString )+import Data.Monoid (mempty, (<>)) +empty :: Doc ann +empty = mempty+ -- class Pretty a where pretty :: a -> Doc -($$) = (<$$>)-x <+> y = x Text.PrettyPrint.Leijen.Text.<+> align (group y)-vcat = align . Text.PrettyPrint.Leijen.Text.vcat . map group-hcat = align . Text.PrettyPrint.Leijen.Text.hcat . map group-vsep = align . Text.PrettyPrint.Leijen.Text.vsep . map group-hsep = align . Text.PrettyPrint.Leijen.Text.hsep . map group-fsep = align . Text.PrettyPrint.Leijen.Text.fillSep . map group-sep = align . Text.PrettyPrint.Leijen.Text.sep . map group-parens = Text.PrettyPrint.Leijen.Text.parens . group-render :: Doc -> String-render = show+x $$ y = D.vcat [x,y]+x <+> y = x D.<+> align y+vcat = align . D.vcat+hcat = align . D.hcat+vsep = align . D.vsep+hsep = align . D.hsep+fsep = align . D.fillSep+sep = align . D.sep -text :: String -> Doc-text = fromString+render = T.renderLazy . renderPretty -{-+renderPretty = D.layoutPretty D.defaultLayoutOptions+renderCompact = D.layoutCompact+renderWide = D.layoutSmart $ D.LayoutOptions { D.layoutPageWidth = D.Unbounded }+displayIO = T.renderIO -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 ]--}+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 ] -{--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--}+-- | WARNING: there is instance Pretty a => Pretty (Maybe a) in the back-end+-- but its spec is "Ignore Nothings, print Just contents" instance ( Pretty a, Pretty b ) => Pretty (Either a b) where pretty (Left x) = text "Left" <+> parens (pretty x)
src/TPDB/XTC.hs view
@@ -2,6 +2,7 @@ ( module TPDB.Data , module TPDB.XTC.Read+, module TPDB.XTC.Write ) @@ -9,4 +10,6 @@ import TPDB.Data import TPDB.XTC.Read+import TPDB.XTC.Write+
src/TPDB/XTC/Read.hs view
@@ -58,7 +58,7 @@ , type_ = ty , startterm = case stt of [] -> Nothing- [x] -> x+ [x] -> Just x , attributes = compute_attributes $ rules rs } @@ -70,15 +70,17 @@ getStrategy = proc x -> do cs <- getText <<< getChildren -< x returnA -< case cs of- "FULL" -> Just Full+ "FULL" -> Just Full+ "INNERMOST" -> Just Innermost+ "OUTERMOST" -> Just Outermost getStartterm = ( proc x -> do getChild "constructor-based" -< x- returnA -< Just Startterm_Constructor_based+ returnA -< Startterm_Constructor_based ) <+> ( proc x -> do getChild "full" -< x- returnA -< Just Startterm_Full- ) <+> ( proc x -> do returnA -< Nothing )+ returnA -< Startterm_Full+ ) getTRS = proc x -> do sig <- getSignature -< x
+ src/TPDB/XTC/Write.hs view
@@ -0,0 +1,62 @@+{-# language OverloadedStrings #-}+{-# language QuasiQuotes #-}++module TPDB.XTC.Write++( document+, writeFile, renderLBS, renderText, def+)++where++import qualified TPDB.Data as D+import qualified Data.Map as M++import qualified Data.Text as T+import qualified Text.XML as X+import Prelude hiding (writeFile)+import Text.XML (writeFile,renderLBS,renderText)+import Text.Hamlet.XML+import Data.Default (def)++document :: D.Problem D.Identifier D.Identifier -> X.Document+document p = X.Document (X.Prologue [] Nothing []) root [] where+ root = X.Element "problem"+ (M.fromList [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")+ ,("type","termination")+ ,("xsi:noNamespaceSchemaLocation","http://dev.aspsimon.org/xtc.xsd")+ ])+ [xml|+<trs>^{trs $ D.trs p}+$maybe s <- D.strategy p+ <strategy>^{strategy s}+|]++strategy s = case s of+ D.Full -> [xml|FULL|]++trs :: D.TRS D.Identifier D.Identifier -> [X.Node]+trs rs = [xml|+<rules>+ $forall u <- D.rules rs+ <rule>+ <lhs>^{term $ D.lhs u}+ <rhs>^{term $ D.rhs u}+<signature>+ $forall f <- D.signature rs+ <funcsym>+ <name>#{T.pack $ show f}+ <arity>#{T.pack $ show $ D.arity f}+|]++term :: D.Term D.Identifier D.Identifier -> [X.Node]+term t = case t of+ D.Var v -> [xml|+<var>#{T.pack $ show v}+|]+ D.Node f args -> [xml|+<funapp>+ <name>#{T.pack $ show f}+ $forall arg <- args+ <arg>^{term arg}+|]
src/TPDB/Xml/Pretty.hs view
@@ -36,12 +36,15 @@ --import Char (isSpace) -- import Text.PrettyPrint.HughesPJ-import TPDB.Pretty hiding ( text )+import TPDB.Pretty hiding ( text, Doc )+import qualified TPDB.Pretty as P import Text.XML.HaXml.Types import Text.XML.HaXml.Namespaces import Data.String ( fromString )++type Doc = P.Doc () text = fromString
+ test/parse_ac.hs view
@@ -0,0 +1,12 @@+import TPDB.Data+import TPDB.Pretty+import TPDB.XTC+import TPDB.Plain.Write++import Control.Monad ( forM, void )++main = void $ do+ [ p ] <- readProblems "test/AC28.xml"+ print $ pretty p+ print $ full_signature p+
+ test/read_complex.hs view
@@ -0,0 +1,12 @@+import TPDB.Data+import TPDB.Pretty+import TPDB.XTC+import TPDB.Plain.Write++import Control.Monad ( forM, void )++main = void $ do+ [ p ] <- readProblems "test/3.39.xml"+ print $ pretty p++
+ test/read_cpf.hs view
@@ -0,0 +1,10 @@+import qualified TPDB.CPF.Proof.Type as CPF+import qualified TPDB.CPF.Proof.Read as CPF+import TPDB.Pretty+import TPDB.Plain.Write++main = do+ s <- readFile "test/AC28.cpf"+ [p] <- CPF.readCP_with_tracelevel 0 s+ print $ pretty $ CPF.input p+
test/read_print_trs.hs view
@@ -4,9 +4,10 @@ import Data.ByteString.Lazy as B import Control.Monad ( forM, void )+import System.IO (stdout) main = void $ do s <- B.readFile "test/33.trs" case trs s of- Right t -> print $ pretty t+ Right t -> displayIO stdout $ renderWide $ pretty t Left err -> error err
tpdb.cabal view
@@ -1,5 +1,5 @@ Name: tpdb-Version: 1.3.3+Version: 1.5.2 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann Category: Logic@@ -28,8 +28,9 @@ -- test/3.15.xml, test/33.trs , test/z001.srs Library- Build-Depends: base==4.*, hxt, wl-pprint-text, text, mtl,- parsec, time, containers, HaXml, filepath, hashable, bytestring+ Build-Depends: base==4.*, hxt, prettyprinter, text, mtl,+ HaXml, xml-hamlet, xml-conduit, data-default,+ parsec, time, containers, filepath, hashable, bytestring if impl(ghc<7.10) build-depends: transformers if impl(ghc<7.10)@@ -42,13 +43,17 @@ TPDB.Mirror TPDB.DP, TPDB.DP.Graph, TPDB.DP.Transform, TPDB.DP.Unify, TPDB.DP.Usable, TPDB.DP.TCap, TPDB.Pretty, TPDB.Plain.Write, TPDB.Plain.Read,- TPDB.XTC, TPDB.XTC.Read, TPDB.Xml, + TPDB.XTC, TPDB.XTC.Read, TPDB.XTC.Write, TPDB.Xml, TPDB.Xml.Pretty, -- TPDB.Rainbow.Proof.Xml, TPDB.Rainbow.Proof.Type TPDB.CPF.Proof.Write, TPDB.CPF.Proof.Read, TPDB.CPF.Proof.Xml, TPDB.CPF.Proof.Type, TPDB.CPF.Proof.Util +Executable plain2xtc+ build-depends: base==4.*, tpdb, bytestring+ main-is: plain2xtc.hs+ -- Executable Compressor -- Main-is: Compressor.hs -- Build-depends: base==4.*, containers >= 0.5, directory, wl-pprint-text, hxt, parsec, hashable@@ -93,5 +98,29 @@ Build-Depends: base==4.*, tpdb Type: exitcode-stdio-1.0 main-is: read_print_xml_theory.hs+ hs-source-dirs: test ++Test-Suite CPF-AC+ Build-Depends: base==4.*, tpdb+ Type: exitcode-stdio-1.0+ main-is: read_cpf.hs+ hs-source-dirs: test ++Test-Suite Parse-AC+ Build-Depends: base==4.*, tpdb+ Type: exitcode-stdio-1.0+ main-is: parse_ac.hs+ hs-source-dirs: test ++Test-Suite read-cpf+ Build-Depends: base==4.*, tpdb+ Type: exitcode-stdio-1.0+ main-is: read_cpf.hs+ hs-source-dirs: test ++Test-Suite read-complex+ Build-Depends: base==4.*, tpdb+ Type: exitcode-stdio-1.0+ main-is: read_complex.hs hs-source-dirs: test