tpdb 1.5.2 → 2.1.0
raw patch · 25 files changed
+348/−619 lines, 25 filesdep +exceptionsdep −HaXmldep −hxtdep −transformers
Dependencies added: exceptions
Dependencies removed: HaXml, hxt, transformers
Files
- src/TPDB/CPF/Proof/Read.hs +91/−78
- src/TPDB/CPF/Proof/Type.hs +10/−9
- src/TPDB/CPF/Proof/Util.hs +2/−1
- src/TPDB/CPF/Proof/Write.hs +26/−31
- src/TPDB/Convert.hs +2/−0
- src/TPDB/Data.hs +5/−4
- src/TPDB/Data/Xml.hs +22/−21
- src/TPDB/Input/File.hs +3/−2
- src/TPDB/Input/Memory.hs +4/−7
- src/TPDB/Plain/Read.hs +14/−14
- src/TPDB/Plain/Write.hs +2/−1
- src/TPDB/XTC/Read.hs +78/−96
- src/TPDB/Xml.hs +48/−25
- src/TPDB/Xml/Pretty.hs +0/−301
- test/attributes.hs +1/−1
- test/parse_ac.hs +1/−1
- test/read_complex.hs +1/−1
- test/read_cpf.hs +1/−2
- test/read_large.hs +12/−0
- test/read_print_srs.hs +2/−2
- test/read_print_trs.hs +2/−2
- test/read_print_trs_2.hs +2/−2
- test/read_print_xml.hs +1/−1
- test/read_print_xml_theory.hs +1/−1
- tpdb.cabal +17/−16
src/TPDB/CPF/Proof/Read.hs view
@@ -1,16 +1,17 @@-{-# language Arrows, NoMonomorphismRestriction, PatternSignatures #-}+{-# language Arrows, NoMonomorphismRestriction, PatternSignatures, OverloadedStrings, LambdaCase #-} 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@@ -18,6 +19,17 @@ import qualified TPDB.CPF.Proof.Write as W -- for testing import qualified Text.XML.HXT.Arrow.XmlState as X +-}++import qualified Text.XML as X+import Text.XML.Cursor+import qualified Data.Text as DT+import qualified Data.Text.Lazy as T+import qualified Data.Text.Lazy.IO as T+import Control.Monad.Catch++import TPDB.Pretty+ {- | dangerous: not all constructor arguments will be set. the function produces something like@@ -27,46 +39,60 @@ } -} -readCP :: String -> IO [ CertificationProblem ]-readCP = readCP_with_tracelevel 0+readCP :: T.Text -> Either SomeException [CertificationProblem]+readCP t = ( fromDoc . fromDocument ) <$> X.parseText X.def t -readCP_with_tracelevel l s = runX ( X.withTraceLevel l $ readString [] s >>> getCP )+readFile :: FilePath -> IO CertificationProblem+readFile f = do+ doc <- X.readFile X.def f+ case fromDoc $ fromDocument doc of+ [] -> error "input contains no certification problem"+ [cp] -> return cp+ cps -> error $ unlines $+ ( "input contains " ++ show (length cps) ++ " certification problems" )+ : map (show . pretty . trsinput_trs . input ) cps -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 }+element1 name c =+ let info = take 100 $ show c+ in case element name c of+ [] -> error $ "missing element " <> show name <> " in " <> info+ [e] -> [e]+ _ -> error $ "more than one element " <> show name <> " in " <> info -getInput = getTerminationInput <+> getComplexityInput <+> getACTerminationInput -getTerminationInput = hasName "input" >>> proc x -> do- trsI <- getTrsInput <<< getChild "trsInput" -< x - returnA -< TrsInput $ RS { rules = trsI, separate = False }+fromDoc :: Cursor -> [ CertificationProblem ]+fromDoc = element1 "certificationProblem" >=> \ c -> + ( CertificationProblem+ <$> (c $/ element "input" &/ getInput )+ <*> (c $/ element "cpfVersion" &/ content )+ <*> (c $/ element "proof" &/ getProof)+ <*> (c $/ element "origin" >=> return [ignoredOrigin] )+ ) -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 }+getInput = getTerminationInput+ <> getComplexityInput+ <> getACTerminationInput++getTerminationInput c = c $| element "trsInput" &/ getTrsInput &| + \ i -> TrsInput $ RS { rules = i , separate = False } ++getACTerminationInput = element "acRewriteSystem" >=> \ c -> do+ let as = c $/ element "Asymbols" &/ getSymbol+ cs = c $/ element "Csymbols" &/ getSymbol+ acrs <- getTrsInput c+ return $ ACRewriteSystem+ { trsinput_trs = RS { rules = acrs, separate = False } , asymbols = as , csymbols = cs } -getSymbol = proc x -> do- s <- getText <<< gotoChild "name" -< x- returnA -< mk 0 s-+getSymbol = element1 "name" &/ \ c -> mk 0 <$> content c -getComplexityInput = hasName "input" >>> proc x -> do- y <- getChild "complexityInput" -< x- trsI <- getTrsInput <<< getChild "trsInput" -< y- cm <- getComplexityMeasure -< y- cc <- getComplexityClass -< y- returnA -< ComplexityInput+getComplexityInput = element "input" >=> \ c -> do+ trsI <- c $/ element "complexityInput" &/ element "trsInput" &/ getTrsInput+ cm <- c $/ getComplexityMeasure + cc <- c $/ getComplexityClass + return $ ComplexityInput { trsinput_trs = RS { rules = trsI, separate = False } , complexityMeasure = cm , complexityClass = cc@@ -74,61 +100,48 @@ getComplexityMeasure = getDummy "derivationalComplexity" DerivationalComplexity- <+> getDummy "runtimeComplexity" RuntimeComplexity+ <> getDummy "runtimeComplexity" RuntimeComplexity -getComplexityClass = proc x -> do- d <- getText <<< gotoChild "polynomial" -< x- returnA -< ComplexityClassPolynomial { degree = read d }+getComplexityClass = element "polynomial" &/ \ c ->+ ( \ s -> ComplexityClassPolynomial { degree = read $ DT.unpack s } ) <$> content c -getTrsInput = proc x -> do- sys <- getTrs <<< getChild "trs" -< x- rels <- listA ( getTrsWith Weak <<< getChild "relativeRules" ) -< x- returnA -< sys ++ concat rels -getTrs = getTrsWith Strict+getTrsInput c =+ ( c $/ element "trs" &/ getRulesWith Strict )+ <> ( c $/ element "relativeRules" &/ getRulesWith Weak ) -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 "acTerminationProof" ( ACTerminationProof undefined )--getDummy t c = proc x -> do - getChild t -< x- returnA -< c +getRulesWith s = element1 "rules" >=> \ c ->+ return ( c $/ ( element "rule" >=> getRule s ) ) -getRules str = proc x -> do- returnA <<< listA ( getRule str <<< getChild "rule" ) -< x+getRule :: Relation -> Cursor -> [ Rule (Term Identifier Identifier) ]+getRule s c = + ( \ l r -> Rule {lhs=l,relation=s,rhs=r,top=False})+ <$> (c $/ element "lhs" &/ getTerm) <*> (c $/ element "rhs" &/ getTerm) -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 }+getProof :: Cursor -> [ Proof ]+getProof c = c $|+ ( getDummy "trsTerminationProof" ( TrsTerminationProof undefined )+ <> getDummy "trsNonterminationProof" ( TrsNonterminationProof undefined )+ <> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined )+ <> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined )+ <> getDummy "complexityProof" ( ComplexityProof undefined )+ <> getDummy "acTerminationProof" ( ACTerminationProof undefined )+ ) +getDummy :: X.Name -> b -> Cursor -> [ b ]+getDummy t c cursor = cursor $| element t >=> return [ c] -getTerm = getVar <+> getFunApp+getTerm :: Cursor -> [ Term Identifier Identifier ]+getTerm = getVar <> getFunApp -getVar = proc x -> do- nm <- getText <<< getChildren <<< hasName "var" -< x- returnA -< Var $ mk 0 nm+getVar :: Cursor -> [ Term Identifier Identifier ]+getVar = element "var" &/ \ c -> ( Var . mk 0 ) <$> content c -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+getFunApp :: Cursor -> [ Term Identifier Identifier ]+getFunApp = element "funapp" >=> \ c -> do+ nm <- c $/ element "name" &/ content+ let args = c $/ element "arg" &/ getTerm+ f = mk (length args) $ nm+ return $ Node f args -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
@@ -19,12 +19,12 @@ import TPDB.Plain.Write () import Data.Typeable import TPDB.Pretty--import Text.XML.HaXml.XmlContent.Haskell hiding ( text )+import Data.Text+import TPDB.Xml (XmlContent) data CertificationProblem = CertificationProblem { input :: CertificationProblemInput - , cpfVersion :: String -- urgh+ , cpfVersion :: Text , proof :: Proof , origin :: Origin } @@ -35,8 +35,8 @@ ignoredOrigin = ProofOrigin { tool = Tool "ignored" "ignored" } -data Tool = Tool { name :: String - , version :: String+data Tool = Tool { name :: Text+ , version :: Text } deriving ( Typeable, Eq ) @@ -80,13 +80,13 @@ | ACTerminationProof ACTerminationProof deriving ( Typeable, Eq ) -data DPS = forall s . ( XmlContent s , Typeable s, Eq s ) +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 ) @@ -231,7 +231,7 @@ data Polynomial = Sum [ Polynomial ] | Product [ Polynomial ] | Polynomial_Coefficient Coefficient- | Polynomial_Variable String+ | Polynomial_Variable Text deriving ( Typeable, Eq ) data ArithFunction = AFNatural Integer@@ -254,7 +254,8 @@ data Coefficient = Vector [ Coefficient ] | Matrix [ Coefficient ]- | forall a . (Eq a, XmlContent a ) => Coefficient_Coefficient a+ | forall a . (Eq a , XmlContent a+ ) => Coefficient_Coefficient a deriving ( Typeable ) instance Eq Coefficient where x == y = error "instance Eq Coefficient"
src/TPDB/CPF/Proof/Util.hs view
@@ -6,6 +6,7 @@ import TPDB.Data import TPDB.CPF.Proof.Type hiding (name) import TPDB.DP +import Data.String (fromString) fromMarkedIdentifier :: Marked Identifier -> Symbol fromMarkedIdentifier = \case @@ -19,7 +20,7 @@ where oldVars = nub $ voccs $ lhs r newVars = zipWith mkNewVar [1..] oldVars- mkNewVar i v = v { name = "x" ++ show i }+ mkNewVar i v = v { name = fromString $ "x" ++ show i } mapping = M.fromList $ zip oldVars newVars mapVar v = case M.lookup v mapping of Just v' -> v'
src/TPDB/CPF/Proof/Write.hs view
@@ -1,4 +1,4 @@-{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}+{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable, OverloadedStrings #-} -- | from internal representation to XML, and back @@ -7,14 +7,8 @@ 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 Text.XML import TPDB.Data.Xml import Data.List ( nub )@@ -22,18 +16,19 @@ import Data.Map (Map) import qualified Data.Map as Map +import qualified Data.Text as T import qualified Data.Time as T import Control.Monad import Data.Typeable import Data.Ratio -tox :: CertificationProblem -> Document ()+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 []+ let style = Instruction+ "xml-stylesheet" "type=\"text/xsl\" href=\"cpfHTML.xsl\""+ pro = Prologue [ MiscInstruction style ] Nothing []+ [ NodeElement e ] = toContents p+ in Document pro e [] instance XmlContent CertificationProblem where parseContents = error "parseContents not implemented"@@ -181,7 +176,7 @@ toContents model = rmkel "model" $ case model of FiniteModel carrierSize interprets -> rmkel "finiteModel" $ concat- [ rmkel "carrierSize" [ nospaceString $ show carrierSize ]+ [ rmkel "carrierSize" $ toContents carrierSize , concatMap toContents interprets ] @@ -226,7 +221,7 @@ , rmkel "realScc" -- $ toContents $ dgcRealScc dgc -- NO, Bool is encoded as text, not as attribute- [ nospaceString $ map toLower $ show $ dgcRealScc dgc ]+ $ toContents $ dgcRealScc dgc ] ++ [ {- rmkel "dpProof" $ -} toContents $ dgcDpProof dgc | dgcRealScc dgc@@ -257,8 +252,8 @@ toContents t = rmkel "matrixInterpretation" $ concat [ toContents ( domain t )- , rmkel "dimension" [ nospaceString $ show $ dimension t ]- , rmkel "strictDimension" [ nospaceString $ show $ strictDimension t ]+ , rmkel "dimension" $ toContents $ dimension t + , rmkel "strictDimension" $ toContents $ strictDimension t ] instance XmlContent Domain where@@ -275,8 +270,8 @@ parseContents = error "parseContents not implemented" toContents r = rmkel "rational" - [ mkel "numerator" [ nospaceString $ show $ numerator r ]- , mkel "denominator" [ nospaceString $ show $ denominator r ]+ [ mkel "numerator" $ toContents $ numerator r + , mkel "denominator" $ toContents $ denominator r ] instance XmlContent Interpret where@@ -284,7 +279,7 @@ toContents i = rmkel "interpret" $ concat [ toContents $ symbol i- , rmkel "arity" [ nospaceString $ show $ arity i ]+ , rmkel "arity" $ toContents $ arity i , toContents $ value i ] @@ -308,8 +303,8 @@ 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 ]+ AFNatural n -> rmkel "natural" $ toContents n + AFVariable n -> rmkel "variable" $ toContents n AFSum afs -> rmkel "sum" $ concatMap toContents afs AFProduct afs -> rmkel "product" $ concatMap toContents afs AFMin afs -> rmkel "min" $ concatMap toContents afs@@ -330,7 +325,7 @@ toContents e = case e of Minus_Infinite -> rmkel "minusInfinity" []- E_Integer i -> rmkel "integer" [ nospaceString $ show i ]+ E_Integer i -> rmkel "integer" $ toContents i Plus_Infinite -> rmkel "plusInfinity" [] -- see remark in TPDB.Data.Xml (sharp_name_HACK)@@ -338,7 +333,7 @@ instance XmlContent Symbol where parseContents = error "parseContents not implemented" - toContents (SymName id) = rmkel "name" [nospaceString $ show id]+ toContents (SymName id) = rmkel "name" $ toContents id toContents (SymSharp sym) = rmkel "sharp" $ toContents sym toContents (SymLabel sym label) = rmkel "labeledSymbol" $ toContents sym ++ (toContents label)@@ -347,7 +342,7 @@ parseContents = error "parseContents not implemented" toContents (LblNumber is) = - rmkel "numberLabel" $ map (\i -> mkel "number" [ nospaceString $ show i ]) is+ rmkel "numberLabel" $ map (\i -> mkel "number" $ toContents i ) is toContents (LblSymbol ss) = rmkel "symbolLabel" $ concatMap toContents ss @@ -365,8 +360,8 @@ toContents (PrecedenceEntry s a p) = rmkel "statusPrecedenceEntry" $ concat [ toContents s- , rmkel "arity" [ nospaceString $ show a ]- , rmkel "precedence" [ nospaceString $ show p ]+ , rmkel "arity" $ toContents a+ , rmkel "precedence" $ toContents p , rmkel "lex" [ ] ] @@ -375,9 +370,9 @@ toContents (ArgumentFilterEntry s a f) = rmkel "argumentFilterEntry" $ concat [ toContents s- , rmkel "arity" [ nospaceString $ show a ]+ , rmkel "arity" $ toContents a , case f of - Left i -> rmkel "collapsing" [ nospaceString $ show i ]+ Left i -> rmkel "collapsing" $ toContents i Right is -> rmkel "nonCollapsing" - $ map (\i -> mkel "position" [ nospaceString $ show i ]) is+ $ map (\i -> mkel "position" $ toContents i) is ]
src/TPDB/Convert.hs view
@@ -1,3 +1,5 @@+{-# language OverloadedStrings #-}+ module TPDB.Convert where import TPDB.Data
src/TPDB/Data.hs view
@@ -24,10 +24,11 @@ import Data.Hashable import Data.Function (on)+import qualified Data.Text as T data Identifier = Identifier { _identifier_hash :: ! Int- , name :: ! String+ , name :: ! T.Text , arity :: Int } deriving ( Eq, Ord, Typeable )@@ -35,9 +36,9 @@ instance Hashable Identifier where hashWithSalt s i = hash (s, _identifier_hash i) -instance Show Identifier where show = name+instance Show Identifier where show = T.unpack . name -mk :: Int -> String -> Identifier+mk :: Int -> T.Text -> Identifier mk a n = Identifier { _identifier_hash = hash (a,n) , arity = a, name = n } @@ -46,7 +47,7 @@ -- | according to XTC spec data Funcsym = Funcsym- { fs_name :: String -- ^ should be Text+ { fs_name :: T.Text , fs_arity :: Int , fs_theory :: Maybe Theory , fs_replacementmap :: Maybe Replacementmap
src/TPDB/Data/Xml.hs view
@@ -1,22 +1,20 @@ {-# language FlexibleContexts #-} {-# language FlexibleInstances #-} {-# language UndecidableInstances #-}+{-# language QuasiQuotes #-} 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 Text.Hamlet.XML+import Data.String import Data.Typeable -- | FIXME: move to separate module instance XmlContent Identifier where- parseContents = do- CString _ s _ <- next - return $ mknullary s+ parseContents = content &| \ c -> mknullary c toContents i = -- probably not here: E.xmlEscape E.stdXmlEscaper -- this introduces whitespace between < and =@@ -24,12 +22,12 @@ -- and this creates a CDATA element -- [ CString True $ show i ] -- so here comes an UGLY HACK:- [ CString False ( escape $ show i ) () ]+ [xml|#{fromString $ escape $ show i}|] -instance ( Typeable ( Term v c ) , XmlContent v, XmlContent c )+instance ( Show v, XmlContent v, XmlContent c ) => XmlContent ( Term v c ) where- toContents ( Var v ) = rmkel "var" $ toContents v+ toContents ( Var v ) = [xml|<var>#{fromString $ show v}|] {- -- for Rainbow: toContents ( Node f xs ) = return $ mkel "app"@@ -51,31 +49,34 @@ -- 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+ toContents ( Node f args ) =+ [xml|<funapp>+ ^{no_sharp_name_HACK ( toContents f )}+ $forall arg <- args+ <arg>^{toContents arg}+ |] + 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 ) ) +instance ( 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- ]+ [xml|<rule>+ <lhs>^{toContents $ lhs u}+ <rhs>^{toContents $ rhs u}+ |]+
src/TPDB/Input/File.hs view
@@ -5,7 +5,8 @@ import qualified TPDB.Input.Memory as TIM -import qualified Data.ByteString.Lazy as B+import qualified Data.Text.Lazy as T+import qualified Data.Text.Lazy.IO as T import System.FilePath.Posix ( takeExtension ) -- | read input from file with given name.@@ -23,7 +24,7 @@ Left err -> error err getE f = do- s <- B.readFile f+ s <- T.readFile f TIM.get f s get_trs f = do
src/TPDB/Input/Memory.hs view
@@ -8,12 +8,12 @@ import TPDB.Plain.Read import TPDB.XTC.Read -import qualified Data.ByteString.Lazy as B+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)-get :: String -> B.ByteString+get :: String -> T.Text -> IO (Either String (Either (TRS Identifier Identifier) (SRS Identifier))) get f s = case takeExtension f of ".srs" -> do@@ -25,8 +25,5 @@ Left err -> return $ Left err Right t -> return $ Right $ Left t _ -> do- ps <- readProblemsBS s- case ps of - [ p ] -> return $ Right $ Left $ TPDB.Data.trs p- [] -> return $ Left "no TRS"- _ -> return $ Left "more than one TRS"+ case readProblemT s of+ Right p -> return $ Right $ Left $ TPDB.Data.trs p
src/TPDB/Plain/Read.hs view
@@ -9,11 +9,9 @@ import Text.Parsec (parse) -import qualified Data.ByteString.Lazy as B-import Data.ByteString.Lazy (ByteString)-import qualified Data.ByteString.Lazy.Char8 as C+import qualified Data.Text.Lazy as T -import Text.Parsec.ByteString.Lazy as P+import Text.Parsec.Text.Lazy as P import Text.Parsec.Token import Text.Parsec.Language import Text.Parsec.Char@@ -23,16 +21,18 @@ import TPDB.Pretty (pretty) import TPDB.Plain.Write ()+import Data.Text ()+import Data.String (fromString) import Control.Monad ( guard, void ) import Data.List ( nub ) -trs :: ByteString -> Either String ( TRS Identifier Identifier )+trs :: T.Text -> 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 :: ByteString -> Either String ( SRS Identifier )+srs :: T.Text -> Either String ( SRS Identifier ) srs s = case Text.Parsec.parse reader "input" s of Left err -> Left $ show err Right t -> Right t@@ -42,7 +42,7 @@ class Reader a where reader :: P.Parser a -- | warning: by definition, {}[] may appear in identifiers-lexer :: GenTokenParser ByteString () Identity+lexer :: GenTokenParser T.Text () Identity lexer = makeTokenParser $ LanguageDef { nestedComments = True@@ -59,7 +59,7 @@ instance Reader Identifier where reader = do i :: String <- identifier lexer - return $ mk 0 i+ return $ mk 0 $ fromString i instance Reader s => Reader [s] where reader = many reader@@ -71,7 +71,7 @@ reader = do f <- reader xs <- ( parens lexer $ commaSep lexer reader ) <|> return []- return $ Node ( f { arity = length xs } ) xs+ return $ Node ( f { arity = Prelude.length xs } ) xs instance Reader u => Reader ( Rule u ) where reader = do@@ -120,13 +120,13 @@ reader = do many space ds <- many $ declaration True- return $ make_srs ds+ return $ make_srs ds instance Reader ( TRS Identifier Identifier ) where reader = do many space ds <- many $ declaration False- return $ make_trs ds+ return $ make_trs ds repair_signature_srs sys = let sig = nub $ do u <- rules sys ; lhs u ++ rhs u@@ -152,9 +152,9 @@ repair_variables vars rules = do let xform ( Node c [] ) | c `elem` vars = Var c- xform ( Node c args ) = Node c ( map xform args )+ xform ( Node c args ) = Node c ( map xform args ) rule <- rules return $ rule { lhs = xform $ lhs rule- , rhs = xform $ rhs rule- }+ , rhs = xform $ rhs rule+ }
src/TPDB/Plain/Write.hs view
@@ -11,9 +11,10 @@ import Data.List ( nub ) import Data.String ( fromString )+import qualified Data.Text as T instance Pretty Identifier where- pretty i = fromString $ name i+ pretty i = pretty $ name i instance ( Pretty v, Pretty s ) => Pretty ( Term v s ) where pretty t = case t of
src/TPDB/XTC/Read.hs view
@@ -1,58 +1,51 @@-{-# language Arrows, NoMonomorphismRestriction, PatternSignatures #-}- -- | construct data object from XML tree. -module TPDB.XTC.Read where+{-# language NoMonomorphismRestriction, PatternSignatures, OverloadedStrings #-} --- implementations follows these examples:--- http://www.haskell.org/haskellwiki/HXT/Practical/ +module TPDB.XTC.Read (readProblemF, readProblemT ) where+ import TPDB.Data import TPDB.Data.Attributes -import Text.XML.HXT.Arrow.XmlArrow+import Text.XML+import Text.XML.Cursor+import qualified Data.Text as ST+import qualified Data.Text.Lazy as LT+import qualified Data.Text.Lazy.IO as LT+import Data.String+import Control.Monad.Catch+import Data.Monoid ((<>)) -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+readProblemF :: FilePath -> IO ( Problem Identifier Identifier )+readProblemF file = do+ doc <- Text.XML.readFile Text.XML.def file+ case getProblem $ fromDocument doc of+ [] -> error "input contains no XTC problem"+ [p] -> return p+ ps -> error "input contains more than one XTC problem" -import qualified Data.ByteString.Lazy as BS-import qualified Data.ByteString.Lazy.Char8 as C-import Text.XML.HXT.IO.GetFILE-import Text.XML.HXT.Arrow.ReadDocument+readProblemT :: LT.Text -> Either SomeException (Problem Identifier Identifier)+readProblemT t = do+ [p] <- ( getProblem . fromDocument ) <$> Text.XML.parseText Text.XML.def t+ return p -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- sig <- getSignature <<< getChild "trs" -< x- returnA -< Problem { trs = rs+getProblem = element "problem" >=> \ c -> do+ let ! ty = case c $| attribute "type" of+ [ "termination" ] -> Termination+ [ "complexity" ] -> Complexity+ _ -> error "type"+ let ! st = case c $/ element "strategy" &/ content of+ [ "FULL" ] -> Just Full+ [ "INNERMOST" ] -> Just Innermost+ [ "OUTERMOST" ] -> Just Outermost+ [] -> Nothing+ _ -> error "strategy"+ rs <- c $/ element "trs" >=> getTRS + let stt = c $/ element "startterm" &/ getStartterm+ sig <- c $/ element "trs" >=> getSignature + return $ Problem { trs = rs , TPDB.Data.strategy = st , TPDB.Data.full_signature = sig , type_ = ty@@ -62,74 +55,63 @@ , attributes = compute_attributes $ rules rs } -getType = proc x -> do- returnA -< case x of- "termination" -> Termination- "complexity" -> Complexity+getTerm :: Cursor -> [ Term Identifier Identifier ]+getTerm = getVar <> getFunApp -getStrategy = proc x -> do- cs <- getText <<< getChildren -< x- returnA -< case cs of- "FULL" -> Just Full- "INNERMOST" -> Just Innermost- "OUTERMOST" -> Just Outermost+getVar :: Cursor -> [ Term Identifier Identifier ]+getVar = element "var" &/ \ c -> ( Var . mk 0 ) <$> content c -getStartterm = ( proc x -> do- getChild "constructor-based" -< x- returnA -< Startterm_Constructor_based- ) <+> ( proc x -> do- getChild "full" -< x- returnA -< Startterm_Full- ) +getFunApp :: Cursor -> [ Term Identifier Identifier ]+getFunApp = element "funapp" >=> \ c -> do+ nm <- c $/ element "name" &/ content+ let args = c $/ element "arg" &/ getTerm+ f = mk (length args) $ nm+ return $ Node f args+ -getTRS = proc x -> do- sig <- getSignature -< x- str <- getRules Strict <<< getChild "rules" -< x- nostr <- listA ( getRules Weak <<< getChild "relrules" <<< getChild "rules" ) -< x+ ++getStartterm =+ (element "constructor-based" &| const Startterm_Constructor_based )+ <> (element "full" &| const Startterm_Full ) ++getTRS c = do+ sig <- getSignature c+ str <- c $/ element "rules" >=> getRulesWith Strict + let nostr = ( c $/ element "relrules" >=> getRulesWith Weak ) -- FIXME: check that symbols are use with correct arity- returnA -< RS { signature = case sig of- Signature fs -> do f <- fs ; return $ mk (fs_arity f) (fs_name f)+ return $ RS { signature = case sig of+ Signature fs -> do f <- fs ; return $ mk (fs_arity f) ( fs_name f) HigherOrderSignature {} -> [] , rules = str ++ concat nostr , separate = False -- for TRS, don't need comma between rules } -getSignature =- ( getFOSignature <<< getChild "signature" )- <+> ( getHOSignature <<< getChild "higherOrderSignature" )--getFOSignature = proc x -> do- fs <- listA ( getFuncsym <<< getChild "funcsym" ) -< x- returnA -< Signature fs+getSignature c = ( c $/ element "signature" >=> getFOSignature )+ <> ( c $/ element "higherOrderSignature" &| const HigherOrderSignature ) -getHOSignature = proc x -> do- returnA -< HigherOrderSignature+getFOSignature c =+ return $ Signature ( c $/ element "funcsym" >=> getFuncsym ) -getFuncsym = proc x -> do- nm <- getText <<< gotoChild "name" -< x- ar <- getRead <<< gotoChild "arity" -< x- th <- listA ( getRead <<< gotoChild "theory" ) -< x- rm <- listA ( listA (getRead <<< gotoChild "entry") <<< gotoChild "replacementmap" ) -< x- returnA -< Funcsym { fs_name = nm+getFuncsym c = do+ nm <- c $/ element "name" &/ content+ ar <- c $/ element "arity" &/ read_content+ let th = c $/ element "theory" &/ read_content+ rm = c $/ element "replacementmap" >=> \ c ->+ return $ c $/ element "entry" &/ read_content+ return $ Funcsym { fs_name = nm , fs_arity = ar , fs_theory = case th of [] -> Nothing ; [t] -> Just t , fs_replacementmap = case rm of [] -> Nothing ; [r] -> Just (Replacementmap r) } -getRead = proc x -> do s <- getText -< x ; returnA -< read s--getRules str = proc x -> do- returnA <<< listA ( getRule str <<< getChild "rule" ) -< x+read_content c = (read . ST.unpack) <$> content c -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 }+getRulesWith s = element "rules" >=> \ c ->+ return ( c $/ ( element "rule" >=> getRule s ) ) -readProblems :: FilePath -> IO [ Problem Identifier Identifier ]-readProblems file =- runX ( readDocument [] file >>> getProblem )+getRule :: Relation -> Cursor -> [ Rule (Term Identifier Identifier) ]+getRule s c = + ( \ l r -> Rule {lhs=l,relation=s,rhs=r,top=False})+ <$> (c $/ element "lhs" &/ getTerm) <*> (c $/ element "rhs" &/ getTerm) -readProblemsBS :: BS.ByteString -> IO [ Problem Identifier Identifier ]-readProblemsBS s =- runX ( readString [] (C.unpack s) >>> getProblem )
src/TPDB/Xml.hs view
@@ -1,26 +1,49 @@-{-# language UndecidableInstances, OverlappingInstances, IncoherentInstances, FlexibleInstances, ScopedTypeVariables #-}--module TPDB.Xml where+{-# language UndecidableInstances, OverlappingInstances, IncoherentInstances, FlexibleInstances, ScopedTypeVariables, OverloadedStrings #-} -import Text.XML.HaXml.Types (QName (..) )-import Text.XML.HaXml.XmlContent.Haskell-import Text.XML.HaXml.Posn ( Posn )+module TPDB.Xml -import qualified Text.XML.HaXml.Pretty as P+( XmlContent (..), mkel, rmkel+, content, (&|)+ , escape, nospaceString+)+ +where import Data.Typeable import Control.Monad import Control.Applicative- -mkel name cs = CElem ( Elem (N name) [] cs ) ()++import Text.XML+import Text.XML.Cursor++import Data.String+import qualified Data.Text as T++class XmlContent a where+ toContents :: a -> [ Node ]+ parseContents :: Cursor -> [a]++instance XmlContent Int where+ toContents = return . nospaceString . fromString . show+instance XmlContent Integer where+ toContents = return . nospaceString . fromString . show+instance XmlContent Bool where+ toContents False = return $ nospaceString "false"+ toContents True = return $ nospaceString "true"++mkel name cs = NodeElement $ Element name mempty cs rmkel name cs = return $ mkel name cs+ +nospaceString :: T.Text -> Node+nospaceString = NodeContent -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@@ -28,7 +51,7 @@ '>' -> ">" ++ escape cs _ -> c : escape cs -+{- type Contents = [ Content Posn ] data CParser a = CParser { unCParser :: Contents -> Maybe ( a, Contents ) }@@ -50,7 +73,7 @@ must_succeed (CParser p ) = CParser $ \ cs -> case p cs of Nothing -> error $ "must succeed:" ++ errmsg cs- ok -> ok+ ok -> ok class Typeable a => XRead a where xread :: CParser a @@ -63,18 +86,18 @@ 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- : []+ $ "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 ]+ ( c : etc ) -> + [ show $ P.content c+ + ]+ _ -> [ show $ length cs ] orelse :: CParser a -> CParser a -> CParser a orelse ( CParser p ) ( CParser q ) = CParser $ \ cs -> @@ -88,8 +111,8 @@ 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 -> Nothing+ Just ( x, _ ) -> Just ( x, etc ) _ -> Nothing strip [] = []@@ -112,5 +135,5 @@ CRef _ _ -> "CRef" CMisc _ _ -> "CMisc" -+-}
− src/TPDB/Xml/Pretty.hs
@@ -1,301 +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, 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--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/attributes.hs view
@@ -6,6 +6,6 @@ import Control.Monad ( forM, void ) main = void $ do- [ p ] <- readProblems "test/3.15.xml"+ p <- readProblemF "test/3.15.xml" print $ pretty p print $ pretty $ attributes p
test/parse_ac.hs view
@@ -6,7 +6,7 @@ import Control.Monad ( forM, void ) main = void $ do- [ p ] <- readProblems "test/AC28.xml"+ p <- readProblemF "test/AC28.xml" print $ pretty p print $ full_signature p
test/read_complex.hs view
@@ -6,7 +6,7 @@ import Control.Monad ( forM, void ) main = void $ do- [ p ] <- readProblems "test/3.39.xml"+ p <- readProblemF "test/3.39.xml" print $ pretty p
test/read_cpf.hs view
@@ -4,7 +4,6 @@ import TPDB.Plain.Write main = do- s <- readFile "test/AC28.cpf"- [p] <- CPF.readCP_with_tracelevel 0 s+ p <- CPF.readFile "test/AC28.cpf" print $ pretty $ CPF.input p
+ test/read_large.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 <- readProblemF "test/MNZ_10_labelled.xml"+ print $ pretty p++
test/read_print_srs.hs view
@@ -2,11 +2,11 @@ import TPDB.Plain.Read import TPDB.Pretty -import Data.ByteString.Lazy as B+import Data.Text.Lazy.IO as T import Control.Monad ( forM, void ) main = void $ do- s <- B.readFile "test/z001.srs"+ s <- T.readFile "test/z001.srs" case srs s of Right t -> print $ pretty t Left err -> error err
test/read_print_trs.hs view
@@ -2,12 +2,12 @@ import TPDB.Plain.Read import TPDB.Pretty -import Data.ByteString.Lazy as B+import Data.Text.Lazy.IO as T import Control.Monad ( forM, void ) import System.IO (stdout) main = void $ do- s <- B.readFile "test/33.trs"+ s <- T.readFile "test/33.trs" case trs s of Right t -> displayIO stdout $ renderWide $ pretty t Left err -> error err
test/read_print_trs_2.hs view
@@ -2,11 +2,11 @@ import TPDB.Plain.Read import TPDB.Pretty -import Data.ByteString.Lazy as B+import Data.Text.Lazy.IO as T import Control.Monad ( forM, void ) main = void $ do- s <- B.readFile "test/02.trs"+ s <- T.readFile "test/02.trs" case trs s of Right t -> print $ pretty t Left err -> error err
test/read_print_xml.hs view
@@ -6,5 +6,5 @@ import Control.Monad ( forM, void ) main = void $ do- [ p ] <- readProblems "test/3.15.xml"+ p <- readProblemF "test/3.15.xml" print $ pretty p
test/read_print_xml_theory.hs view
@@ -6,6 +6,6 @@ import Control.Monad ( forM, void ) main = void $ do- [ p ] <- readProblems "test/AC09.xml"+ p <- readProblemF "test/AC09.xml" print $ pretty p print $ full_signature p
tpdb.cabal view
@@ -1,5 +1,5 @@ Name: tpdb-Version: 1.5.2+Version: 2.1.0 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann Category: Logic@@ -28,13 +28,9 @@ -- test/3.15.xml, test/33.trs , test/z001.srs Library- 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)- Extensions: DeriveDataTypeable+ Build-Depends: base==4.*, prettyprinter, text, mtl,+ xml-hamlet, xml-conduit, data-default,+ parsec, time, containers, filepath, hashable, bytestring, exceptions Hs-Source-Dirs: src Exposed-Modules: TPDB.Data, TPDB.Data.Term, TPDB.Data.Rule, TPDB.Data.Attributes, TPDB.Data.Xml@@ -44,8 +40,6 @@ 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.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@@ -65,31 +59,32 @@ hs-source-dirs: test Test-Suite TRS- Build-Depends: base==4.*, tpdb, bytestring+ Build-Depends: base==4.*, tpdb, text Type: exitcode-stdio-1.0 main-is: read_print_trs.hs hs-source-dirs: test Test-Suite TRS_02- Build-Depends: base==4.*, tpdb, bytestring+ Build-Depends: base==4.*, tpdb, text Type: exitcode-stdio-1.0 main-is: read_print_trs_2.hs hs-source-dirs: test Test-Suite SRS- Build-Depends: base==4.*, tpdb, bytestring+ Build-Depends: base==4.*, tpdb, text Type: exitcode-stdio-1.0 main-is: read_print_srs.hs hs-source-dirs: test Test-Suite Speed- Build-Depends: base==4.*, tpdb, HaXml, bytestring, pretty+ Buildable: False+ Build-Depends: base==4.*, tpdb, text, pretty Type: exitcode-stdio-1.0 main-is: speed.hs hs-source-dirs: test -+ Test-Suite Attributes- Build-Depends: base==4.*, tpdb, HaXml, bytestring, pretty+ Build-Depends: base==4.*, tpdb, text, pretty Type: exitcode-stdio-1.0 main-is: attributes.hs hs-source-dirs: test @@ -122,5 +117,11 @@ Build-Depends: base==4.*, tpdb Type: exitcode-stdio-1.0 main-is: read_complex.hs+ hs-source-dirs: test ++Test-Suite read-large+ Build-Depends: base==4.*, tpdb+ Type: exitcode-stdio-1.0+ main-is: read_large.hs hs-source-dirs: test