tpdb 0.6.1 → 0.7.1
raw patch · 16 files changed
+471/−312 lines, 16 filesdep +bytestringdep +hashabledep +wl-pprint-textdep −directory
Dependencies added: bytestring, hashable, wl-pprint-text
Dependencies removed: directory
Files
- Compressor.hs +0/−80
- TPDB/CPF/Proof/Type.hs +1/−1
- TPDB/CPF/Proof/Xml.hs +1/−0
- TPDB/Compress.hs +0/−179
- TPDB/Convert.hs +6/−3
- TPDB/DP.hs +13/−2
- TPDB/Data.hs +9/−2
- TPDB/Input.hs +21/−5
- TPDB/Plain/Read.hs +1/−1
- TPDB/Plain/Write.hs +11/−8
- TPDB/Pretty.hs +34/−3
- TPDB/Rainbow/Proof/Type.hs +16/−14
- TPDB/XTC/Read.hs +3/−3
- TPDB/Xml/Pretty.hs +298/−0
- test/speed.hs +40/−0
- tpdb.cabal +17/−11
− Compressor.hs
@@ -1,80 +0,0 @@-{-# language DoAndIfThenElse #-}--import TPDB.Compress (compress)-import TPDB.DP ( dp, Marked (Auxiliary) )-import TPDB.Data-import TPDB.XTC.Read ( readProblems )-import TPDB.Plain.Write ( )-import TPDB.Pretty ( pretty )-import Text.PrettyPrint.HughesPJ - ( text, ($$), nest, vcat )--import System.Environment-import System.IO-import System.Directory-import Control.Monad ( guard, forM )-import Data.List ( isSuffixOf, isPrefixOf )-import qualified Data.Set as S---- | give file/dir name(s) on cmd line.--- recursively collect all *.xml files,--- and apply TRS compression.--main = do- hSetBuffering stdout LineBuffering - args <- getArgs- ss <- collect args- putStrLn "action"- forM ( map dp ss ) $ \ s -> do- print $ text "original TRS" </> pretty s - let ( com, rules ) = compress supply s- print $ text "compressed TRS" </> vcat- ( pretty com : map pretty rules )- print $ judge s--p </> q = p $$ nest 4 q--judge sys = - let csys = compress supply sys- in ( cost_trs sys , cost_comp csys )--supply = do - i <- [ 0 .. ] - return $ Auxiliary $ mknullary $ "c" ++ show i--cost_comp ( s, sub ) = - cost_trs s + cost_sub sub- -cost_sub sub = sum $ do- ((f, af), Just (g, k, h, ca)) <- sub- return ca--cost_trs s = sum $ do- u <- rules s- t <- [ lhs u, rhs u ]- return $ cost_term t--cost_term t = sum $ do - (p,s) <- positions t - return $ multiplications s--multiplications t = case t of- Node f xs -> sum $ do- x @ Node {} <- xs- return $ S.size $ vars x- _ -> 0 --collect fs = do- let special d = isPrefixOf "." d- fss <- forM fs $ \ f -> do- d <- doesDirectoryExist f- if d - then do- fs <- getDirectoryContents f- collect $ map ( ( f ++ "/" ) ++ )- $ filter (not . special) fs- else if isSuffixOf ".xml" f- then fmap (map trs) $ readProblems f- else return []- return $ concat fss-
TPDB/CPF/Proof/Type.hs view
@@ -42,7 +42,7 @@ deriving ( Typeable ) data Sharp i = Sharp i | Plain i- deriving ( Typeable )+ deriving ( Typeable, Eq, Ord ) data DPS = forall s . ( XmlContent s , Typeable s ) => DPS [ Rule (Term Identifier s) ]
TPDB/CPF/Proof/Xml.hs view
@@ -83,6 +83,7 @@ instance XmlContent TrsTerminationProof where toContents p = rmkel "trsTerminationProof" $ case p of+ RIsEmpty -> rmkel "rIsEmpty" [] DpTrans {} -> rmkel "dpTrans" $ toContents ( dptrans_dps p ) ++ rmkel "markedSymbols" [ CString False "true" () ]
− TPDB/Compress.hs
@@ -1,179 +0,0 @@-{-# language TemplateHaskell #-}--module TPDB.Compress where--import TPDB.Data hiding ( trs, arity )-import TPDB.Plain.Write ()-import qualified TPDB.Plain.Read (trs) -- for testing-import TPDB.Pretty --import Control.Monad ( guard ) -import qualified Data.Set as S-import qualified Data.Map.Strict as M-import Data.List ( sortBy )-import Data.Ord ( comparing )----- | compute a compressed version of the TRS.--- Warning: in the output, the arities of fresh identifiers will be nonsensical-compress :: ( Ord s )- => [s] -- ^ supply of function symbols. This can be any infinite list,- -- the implementation will filter out those elements that- -- occur in the original TRS's signature.- -> TRS v s - -> ( TRS v s - , [ ((s, Int), Maybe (s,Int,s,Int) ) ] - ) -- ^ ((f, a), Just (g,i,h,a)) semantics: new function symbols f- -- by substituting h in the i-th position (start at 0) of g.- -- arity of child is a- -- ((f, a), Nothing ) semantics: f of arity a is an "old" function symbol.- -- output is in dependency order (will only refer to previously defined symbols).-compress pool sys = - let osig = ohsig sys- forbidden = M.keysSet osig- fresh = filter ( `S.notMember` forbidden ) pool- con = make fresh sys- in ( trs con - , map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig )- ++ map ( \ (f, p) -> ( (f, arity p), Just (parent p, branch p, child p, child_arity p) ) ) - ( reverse $ defs con )- )--ohsig sys = M.fromListWith ( \ o n -> if o == n then o else error "different arities" ) - $ do u <- rules sys ; t <- [ lhs u , rhs u ]- ( _ , Node f args ) <- positions t- return ( f, length args )--dont_compress pool sys = - let osig = ohsig sys- in ( sys , map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig ) )- --data Pattern s = Pattern- { parent :: ! s- , branch :: ! Int- , child :: ! s- , arity :: ! Int- , child_arity :: ! Int- , has_grand_child :: ! Bool - }- deriving ( Eq, Ord )--data Container v s = Container - { trs :: TRS v s- , defs :: [( s, Pattern s)] - }--make fresh trs = handle fresh $ Container trs []---handle free con = - case -- take 1 $ - disjoint $ best_patterns $ trs con of- [] -> con- ps -> - let ( pre, post ) - = splitAt ( length ps ) free- here = zip pre ps - in handle post- $ con { trs = apply_system here $ trs con- , defs = here ++ defs con- }--patterns_in_term t = - nonoverlapping t ++ overlapping t--overlapping t = do- (pos, Node f xs) <- positions t- ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs- guard $ f == g- let sub = case ys !! k of - Node h _ -> True- _ -> False- guard $ if sub then even $ length pos else True - let r = not $ null $ do Node {} <- ys ; return ()- return $ Pattern { arity = length xs - 1 + length ys- , parent = f, branch = k- , child = g, child_arity = length ys- , has_grand_child = r - }--nonoverlapping t = do- Node f xs <- subterms t- ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs- guard $ f /= g- let r = not $ null $ do Node {} <- ys ; return ()- return $ Pattern { arity = length xs - 1 + length ys- , parent = f, branch = k- , child = g, child_arity = length ys- , has_grand_child = r - }--patterns_in_rule u = do- t <- [ lhs u, rhs u ]- patterns_in_term t--patterns trs = do- u <- rules trs- patterns_in_rule u--disjoint ps =- let h seen [] = []- h seen (p:ps) = - if S.notMember (parent p) seen- && S.notMember (child p) seen- then p : h (S.insert (parent p) - $ S.insert (child p) seen) ps- else h seen ps - in h S.empty ps --best_patterns trs = do- let pns = sortBy ( comparing ( negate . snd ))- $ M.toList $ collect $ patterns trs- let threshold = case pns of - [] -> 0- (p,n) : _ -> div n 2- (p,n) <- takeWhile ( \ (p,n) -> n >= threshold ) pns- guard $ ( n > 1 ) || ( n == 1 && has_grand_child p )- return p---apply_system fgps trs = do- trs { rules = map ( apply_rule fgps ) $ rules trs }--apply_rule fgps u = - u { lhs = apply_term fgps $ lhs u- , rhs = apply_term fgps $ rhs u- }--apply_term _ ( Var v ) = Var v-apply_term fgps t @ (Node top args) = - let Node newtop newargs = multi_matches fgps t- in Node newtop $ map (apply_term fgps) newargs- -multi_matches [] t = t-multi_matches ((fg, p@Pattern{parent=f,branch=i,child=g}) : fgps ) t@(Node top args) = - if matches p t- then let ( pre, Node _ sub : post) = splitAt i args - in Node fg ( pre ++ sub ++ post ) - else multi_matches fgps t --matches ( Pattern { parent = f, branch = i, child = g } ) - ( Node top args ) | top == f = - case args !! i of- Node bot _ | bot == g -> True- _ -> False-matches p _ = False----collect xs = M.fromListWith (+) $ do - x <- xs - return ( x, child_arity x )---invert :: ( Ord a, Ord b )- => M.Map a b -> M.Map b [a]-invert fm = M.fromListWith (++) $ do- ( k, v ) <- M.toList fm- return ( v, [k] )
TPDB/Convert.hs view
@@ -9,7 +9,7 @@ } convert_srs_rule u = - let v = Identifier "x" 0 + let v = mk 0 "x" in u { lhs = unspine v $ lhs u , rhs = unspine v $ rhs u } @@ -28,9 +28,12 @@ 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 [ a ] -> do- ( sp, base ) <- spine a + Node f args -> do+ [ arg ] <- return args+ ( sp, base ) <- spine arg return ( f : sp, base ) Var v -> return ( [] , v )
TPDB/DP.hs view
@@ -1,19 +1,30 @@+{-# language OverloadedStrings #-}+ module TPDB.DP where import TPDB.Data import TPDB.Pretty-import Text.PrettyPrint.HughesPJ+import TPDB.Pretty import qualified Data.Set as S import Control.Monad ( guard ) +import Data.Hashable+import GHC.Generics+ data Marked a = Original a | Marked a | Auxiliary a deriving ( Eq, Ord ) +instance Hashable a => Hashable (Marked a) where+ hashWithSalt s m = case m of+ Original x -> hashWithSalt s $ hashWithSalt (0::Int) x+ Marked x -> hashWithSalt s $ hashWithSalt (1::Int) x+ Auxiliary x -> hashWithSalt s $ hashWithSalt (2::Int) x+ instance Pretty a => Pretty ( Marked a) where pretty m = case m of Original a -> pretty a- Marked a -> pretty a <> text "#"+ Marked a -> pretty a <> "#" Auxiliary a -> pretty a dp s =
TPDB/Data.hs view
@@ -14,14 +14,21 @@ import Data.Typeable import Control.Monad ( guard ) +import Data.Hashable -data Identifier = Identifier { name :: String , arity :: Int }+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 { arity = a, name = n }+mk a n = Identifier { _identifier_hash = hash (a,n)+ , arity = a, name = n } ---------------------------------------------------------------------
TPDB/Input.hs view
@@ -14,28 +14,44 @@ -> 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 = do let ( base, ext ) = splitExtension f case ext of ".srs" -> do s <- readFile f case srs s of- Left err -> error err- Right t -> return $ Right t+ 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 -> error err- Right t -> return $ Left t + Left err -> return $ Left err+ Right t -> return $ Right $ Left t ".xml" -> do ps <- readProblems f case ps of - [ p ] -> return $ Left $ TPDB.Data.trs p+ [ 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
TPDB/Plain/Read.hs view
@@ -41,7 +41,7 @@ instance Reader Identifier where reader = do i <- identifier lexer - return $ Identifier { arity = 0 , name = i }+ return $ mk 0 i instance Reader s => Reader [s] where reader = many reader
TPDB/Plain/Write.hs view
@@ -2,17 +2,18 @@ -- 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 Text.PrettyPrint.HughesPJ import Data.List ( nub )+import Data.String ( fromString ) instance Pretty Identifier where- pretty i = text $ name i+ pretty i = fromString $ name i instance ( Pretty v, Pretty s ) => Pretty ( Term v s ) where pretty t = case t of@@ -24,9 +25,9 @@ instance PrettyTerm a => Pretty ( Rule a ) where pretty u = hsep [ prettyTerm $ lhs u , case relation u of - Strict -> text "->" - Weak -> text "->="- Equal -> text "="+ Strict -> "->" + Weak -> "->="+ Equal -> "=" -- FIXME: implement "top" annotation , prettyTerm $ rhs u ]@@ -42,7 +43,7 @@ instance ( Pretty s, PrettyTerm r ) => Pretty ( RS s r ) where pretty sys = vcat - [ parens $ text "RULES" <+>+ [ parens $ "RULES" <+> vcat ( ( if separate sys then punctuate comma else id ) $ map pretty $ rules sys )@@ -57,8 +58,10 @@ [ pretty $ trs p , case strategy p of Nothing -> empty- Just s -> fsep [ text "strategy", text ( show s ) ]+ Just s -> fsep [ "strategy"+ , fromString ( show s ) ] , case startterm p of Nothing -> empty- Just s -> fsep [ text "startterm", text ( show s ) ] + Just s -> fsep [ "startterm"+ , fromString ( show s ) ] ]
TPDB/Pretty.hs view
@@ -1,9 +1,37 @@-module TPDB.Pretty where+module TPDB.Pretty -import Text.PrettyPrint.HughesPJ+( Doc, SimpleDoc+, render, renderCompact, displayIO+, Pretty (..)+, fsep , hsep, vsep, vcat, hcat+, parens, brackets, angles, braces, enclose+, punctuate, comma, nest+, empty, text+, (<>), (<+>), ($$)+) -class Pretty a where pretty :: a -> Doc+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@@ -11,10 +39,12 @@ 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 @@ -22,3 +52,4 @@ pretty m = case m of Nothing -> text "Nothing" Just x -> text "Just" <+> pretty x -- FIXME: parens missing+-}
TPDB/Rainbow/Proof/Type.hs view
@@ -1,4 +1,6 @@-{-# OPTIONS -fglasgow-exts #-}+{-# language OverloadedStrings #-}+{-# language ExistentialQuantification #-}+{-# language DeriveDataTypeable #-} -- | internal representation of Rainbow termination proofs, -- see <http://color.loria.fr/>@@ -11,7 +13,6 @@ import TPDB.Data hiding ( Type (..)) import TPDB.Pretty import TPDB.Plain.Write () -- just instances-import Text.PrettyPrint.HughesPJ import qualified TPDB.CPF.Proof.Type as C @@ -20,6 +21,7 @@ import qualified Data.Time as T import Data.Typeable+import Data.String (fromString) data Vector a = Vector [ a ] deriving Typeable@@ -64,9 +66,9 @@ data Domain = Natural | Arctic | Arctic_Below_Zero | Tropical deriving ( Show, Eq, Ord, Typeable ) -instance Pretty Domain where pretty = text . show-instance Pretty T.NominalDiffTime where pretty = text . show-instance Pretty T.UTCTime where pretty = text . show+instance Pretty Domain where pretty = fromString . show+instance Pretty T.NominalDiffTime where pretty = fromString . show+instance Pretty T.UTCTime where pretty = fromString . show data Red_Ord = Red_Ord_Matrix_Int Matrix_Int@@ -79,14 +81,14 @@ deriving Typeable instance Pretty Usable_Rules where - pretty (Usable_Rules sp) = text "Usable_Rules" <+> pretty sp+ pretty (Usable_Rules sp) = "Usable_Rules" <+> pretty sp data Simple_Projection = Simple_Projection [ ( Identifier, Int ) ] deriving Typeable instance Pretty Simple_Projection where - pretty (Simple_Projection sp) = text "Simple_Projection" <+> pretty sp+ pretty (Simple_Projection sp) = "Simple_Projection" <+> pretty sp data Claim = Claim { system :: TRS Identifier Identifier@@ -110,9 +112,9 @@ instance Pretty Property where pretty p = case p of- Termination -> text "YES # Termination"- Top_Termination -> text "YES # Top_Termination"- Complexity ( lo, hi ) -> text "YES" <+> pretty ( lo, hi ) + Termination -> "YES # Termination"+ Top_Termination -> "YES # Top_Termination"+ Complexity ( lo, hi ) -> "YES" <+> pretty ( lo, hi ) -- | see specification: -- http://termination-portal.org/wiki/Complexity@@ -126,13 +128,13 @@ instance Pretty Function where pretty f = case f of- Unknown -> text "?"+ Unknown -> "?" Polynomial { degree = Nothing } -> - text "POLY"+ "POLY" Polynomial { degree = Just 0 } -> - text "O(1)"+ "O(1)" Polynomial { degree = Just d } -> - text "O" <+> parens ( text "n^" <> pretty d)+ "O" <+> parens ( "n^" <> pretty d)
TPDB/XTC/Read.hs view
@@ -25,13 +25,13 @@ getVar = proc x -> do nm <- getText <<< getChildren <<< hasName "var" -< x- returnA -< Var $ Identifier { name = nm, arity = 0 }+ 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 = Identifier { name = nm, arity = length gs }+ let c = mk (length gs) nm returnA -< Node c gs gotoChild tag = proc x -> do@@ -90,7 +90,7 @@ getFuncsym = proc x -> do nm <- getText <<< gotoChild "name" -< x ar <- getText <<< gotoChild "arity" -< x- returnA -< Identifier { name = nm , arity = read ar }+ returnA -< mk (read ar) nm getRules str = proc x -> do returnA <<< listA ( getRule str <<< getChild "rule" ) -< x
+ 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
@@ -0,0 +1,40 @@+import Text.XML.HaXml++import qualified Text.XML.HaXml.Pretty as P+import qualified Text.XML.HaXml.ByteStringPP as BSP+import qualified Data.ByteString.Lazy.Char8 as BS+import Text.PrettyPrint.HughesPJ hiding ( int, double )++import qualified TPDB.Pretty as TP+import qualified TPDB.Xml.Pretty as TXP++import System.IO ( stdout )+import System.Environment ( getArgs )++mkel name cs = CElem ( Elem (N name) [] cs ) ()+rmkel name cs = return $ mkel name cs++list xs = foldr ( \ x y -> rmkel "cons" + [ mkel "head" x , mkel "tail" y ] )+ ( rmkel "nil" [] ) xs++int i = [ CElem (Elem (N "int") + [ (N "val", AttValue [ Left $ show i] ) ] []) () ]++double n = header+ $ list $ replicate n + $ list $ replicate n $ int 42++header l =+ let xd = XMLDecl "1.0" + ( Just $ EncodingDecl "UTF-8" ) Nothing + pro = Prolog ( Just xd ) [] Nothing []+ [ 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+ TP.displayIO stdout $ TP.renderCompact $ TXP.document+ $ double 132
tpdb.cabal view
@@ -1,5 +1,5 @@ Name: tpdb-Version: 0.6.1+Version: 0.7.1 Author: Johannes Waldmann Maintainer: Johannes Waldmann Category: Science@@ -26,38 +26,44 @@ -- test/3.15.xml, test/33.trs , test/z001.srs Library- Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml, filepath+ Build-Depends: base==4.*, hxt, wl-pprint-text, + parsec, time, containers, HaXml, filepath, hashable Exposed-Modules: TPDB.Data, TPDB.Data.Term, TPDB.Data.Xml- TPDB.Compress, TPDB.Convert, TPDB.Input+ -- TPDB.Compress, + TPDB.Convert, TPDB.Input TPDB.Mirror, TPDB.DP TPDB.Pretty, TPDB.Plain.Write, TPDB.Plain.Read, TPDB.XTC, TPDB.XTC.Read, TPDB.Xml, + TPDB.Xml.Pretty, TPDB.Rainbow.Proof.Xml, TPDB.Rainbow.Proof.Type TPDB.CPF.Proof.Xml, TPDB.CPF.Proof.Type -Executable Compressor- Main-is: Compressor.hs- Build-depends: base==4.*, containers >= 0.5, directory, pretty, hxt, parsec+-- Executable Compressor+-- Main-is: Compressor.hs+-- Build-depends: base==4.*, containers >= 0.5, directory, wl-pprint-text, hxt, parsec, hashable Test-Suite XML- Build-Depends: base==4.*, hxt, pretty, parsec, time, containers >= 0.5, HaXml+ Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers >= 0.5, HaXml, hashable Type: exitcode-stdio-1.0 main-is: read_print_xml.hs hs-source-dirs: test . Test-Suite TRS- Build-Depends: base==4.*, hxt, pretty, parsec, time, containers >= 0.5, HaXml+ Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers >= 0.5, HaXml, hashable Type: exitcode-stdio-1.0 main-is: read_print_trs.hs hs-source-dirs: test . Test-Suite SRS- Build-Depends: base==4.*, hxt, pretty, parsec, time, containers >= 0.5, HaXml+ Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers >= 0.5, HaXml, hashable Type: exitcode-stdio-1.0 main-is: read_print_srs.hs- hs-source-dirs: test . -+Test-Suite Speed+ Build-Depends: base==4.*, hxt, wl-pprint-text, parsec, time, containers >= 0.5, HaXml, hashable, pretty,bytestring+ Type: exitcode-stdio-1.0+ main-is: speed.hs+ hs-source-dirs: test .