diff --git a/TPDB/CPF/Proof/Type.hs b/TPDB/CPF/Proof/Type.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/CPF/Proof/Type.hs
@@ -0,0 +1,105 @@
+{-# OPTIONS -fglasgow-exts #-}
+
+-- | internal representation of CPF termination proofs,
+-- see
+
+module TPDB.CPF.Proof.Type
+
+( module TPDB.CPF.Proof.Type
+, Identifier
+, TES
+)
+
+where
+
+import TPDB.Data
+import Data.Typeable
+
+import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
+
+data CertificationProblem =
+ CertificationProblem { input :: CertificationProblemInput
+ , proof :: Proof }
+ deriving ( Typeable )
+
+data CertificationProblemInput
+ = TrsInput { trsinput_trs :: TRS Identifier Identifier }
+ -- ^ this is actually not true, since instead of copying from XTC,
+ -- CPF format repeats the definition of TRS,
+ -- and it's a different one (relative rules are extra)
+ deriving ( Typeable )
+
+data Proof = TrsTerminationProof TrsTerminationProof
+ -- | TrsNonterminationProof
+ deriving ( Typeable )
+
+data Sharp i = Sharp i | Plain i
+ deriving ( Typeable )
+
+data DPS = forall s . ( XmlContent s , Typeable s )
+ => DPS [ Rule (Term Identifier s) ]
+ deriving ( Typeable )
+
+data TrsTerminationProof
+ = RIsEmpty
+{-
+ | RuleRemoval { orderingConstraintProof :: OrderingConstraintProof
+ , trs :: TRS Identifier Identifier
+ , trsTerminationProof :: TrsTerminationProof
+ }
+-}
+ | DpTrans { dptrans_dps :: DPS
+ , markedSymbols :: Bool , dptrans_dpProof :: DpProof }
+ | StringReversal { trs :: TRS Identifier Identifier
+ , trsTerminationProof :: TrsTerminationProof
+ }
+ deriving ( Typeable )
+
+data DpProof = PIsEmpty
+ | RedPairProc { orderingConstraintProof :: OrderingConstraintProof
+ , red_pair_dps :: DPS , redpairproc_dpProof :: DpProof }
+ deriving ( Typeable )
+
+data OrderingConstraintProof
+ = RedPair { interpretation :: Interpretation }
+ deriving ( Typeable )
+
+data Interpretation =
+ Interpretation { interpretation_type :: Interpretation_Type
+ , interprets :: [ Interpret ]
+ }
+ deriving ( Typeable )
+
+data Interpretation_Type =
+ Matrix_Interpretation { domain :: Domain, dimension :: Int
+ , strictDimension :: Int
+ }
+ deriving ( Typeable )
+
+data Domain = Naturals
+ deriving ( Typeable )
+
+data Interpret = forall s . XmlContent s => Interpret
+ { symbol :: s , arity :: Int , value :: Value }
+ deriving ( Typeable )
+
+data Value = Polynomial Polynomial
+ deriving ( Typeable )
+
+data Polynomial = Sum [ Polynomial ]
+ | Product [ Polynomial ]
+ | Polynomial_Coefficient Coefficient
+ deriving ( Typeable )
+
+data Coefficient = Vector [ Coefficient ]
+ | Matrix [ Coefficient ]
+ | forall a . XmlContent a => Coefficient_Coefficient a
+ deriving ( Typeable )
+
+
+
+
+
+
+
+
diff --git a/TPDB/CPF/Proof/Xml.hs b/TPDB/CPF/Proof/Xml.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/CPF/Proof/Xml.hs
@@ -0,0 +1,134 @@
+{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}
+
+-- | from internal representation to XML, and back
+
+module TPDB.CPF.Proof.Xml where
+
+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(..) )
+
+import TPDB.Xml
+import TPDB.Data.Xml
+
+import Data.List ( nub )
+import Data.Char ( toLower )
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import qualified Data.Time as T
+import Control.Monad
+import Data.Typeable
+
+tox :: CertificationProblem -> Document ()
+tox p =
+ let xd = XMLDecl "1.0" ( Just $ EncodingDecl "UTF-8" ) Nothing
+ pro = Prolog ( Just xd ) [] Nothing []
+ [ CElem e _ ] = toContents p
+ in Document pro emptyST e []
+
+instance XmlContent CertificationProblem where
+ toContents cp = rmkel "certificationProblem"
+ [ mkel "input" $ toContents ( input cp )
+ , mkel "proof" $ toContents ( proof cp )
+ ]
+
+instance XmlContent CertificationProblemInput where
+ toContents i = case i of
+ TrsInput {} -> rmkel "trsInput" $ toContents ( trsinput_trs i )
+
+instance ( Typeable v, Typeable c, XmlContent v , XmlContent c )
+ => XmlContent ( T.TRS v c ) where
+ toContents s = rmkel "trs"
+ $ rmkel "rules" $ concat $ map toContents $ T.rules s
+
+instance ( Typeable t, XmlContent t )
+ => XmlContent ( T.Rule t) where
+ toContents u = rmkel "rule" $
+ rmkel "lhs" ( toContents $ T.lhs u )
+ ++ rmkel "rhs" ( toContents $ T.rhs u )
+
+
+instance XmlContent Proof where
+ toContents p = case p of
+ TrsTerminationProof p -> toContents p
+
+instance ( Typeable i , XmlContent i ) => XmlContent ( Sharp i ) where
+ toContents s = case s of
+ Plain p -> toContents p
+ Sharp q -> rmkel "sharp" $ toContents q
+
+instance XmlContent DPS where
+ toContents ( DPS rules ) = rmkel "dps" $ concat $ map toContents rules
+
+instance XmlContent TrsTerminationProof where
+ toContents p = rmkel "trsTerminationProof" $ case p of
+ DpTrans {} -> rmkel "dpTrans" $
+ toContents ( dptrans_dps p )
+ ++ rmkel "markedSymbols" [ CString False "true" () ]
+ ++ toContents ( dptrans_dpProof p )
+
+instance XmlContent DpProof where
+ toContents p = rmkel "dpProof" $ case p of
+ PIsEmpty -> rmkel "pIsEmpty" []
+ RedPairProc {} -> rmkel "redPairProc"
+ $ toContents ( orderingConstraintProof p )
+ ++ toContents ( red_pair_dps p )
+ ++ toContents ( redpairproc_dpProof p )
+
+instance XmlContent OrderingConstraintProof where
+ toContents p = rmkel "orderingConstraintProof" $ case p of
+ RedPair {} -> rmkel "redPair" $ toContents ( interpretation p )
+
+instance XmlContent Interpretation where
+ toContents i = rmkel "interpretation" $
+ rmkel "type" ( toContents $ interpretation_type i )
+ ++ concat ( map toContents $ interprets i )
+
+instance XmlContent Interpretation_Type where
+ toContents t = rmkel "matrixInterpretation" $
+ toContents ( domain t )
+ ++ rmkel "dimension"
+ [ CString False ( show ( dimension t )) () ]
+ ++ rmkel "strictDimension"
+ [ CString False ( show ( strictDimension t )) () ]
+
+instance XmlContent Domain where
+ toContents d = rmkel "domain" $ case d of
+ Naturals -> rmkel "naturals" []
+
+instance XmlContent Interpret where
+ toContents i = rmkel "interpret" $ case i of
+ Interpret { symbol = s } ->
+ toContents s
+ ++ rmkel "arity" [ CString False ( show ( arity i )) () ]
+ ++ toContents ( value i )
+
+instance XmlContent Value where
+ toContents v = case v of
+ Polynomial p -> toContents p
+
+instance XmlContent Polynomial where
+ toContents p = rmkel "polynomial" $ case p of
+ Sum ps -> rmkel "sum" $ concat ( map toContents ps )
+ Product ps -> rmkel "product" $ concat ( map toContents ps )
+ Polynomial_Coefficient c -> rmkel "coefficient" $ toContents c
+
+instance XmlContent Coefficient where
+ toContents v = case v of
+ Matrix vs -> rmkel "matrix" $ concat ( map toContents vs )
+ Vector cs -> rmkel "vector" $ concat ( map toContents cs )
+ Coefficient_Coefficient i ->
+ rmkel "coefficient" $ toContents i
+
+
+
+
+
+
diff --git a/TPDB/Data.hs b/TPDB/Data.hs
--- a/TPDB/Data.hs
+++ b/TPDB/Data.hs
@@ -1,39 +1,88 @@
-module TPDB.Data where
+{-# language DeriveDataTypeable #-}
+module TPDB.Data
+
+( module TPDB.Data
+, module TPDB.Data.Term
+)
+
+where
+
+
+import TPDB.Data.Term
+
+import Data.Typeable
+import Control.Monad ( guard )
+
+
data Identifier = Identifier { name :: String , arity :: Int }
- deriving ( Eq, Ord, Show )
+ deriving ( Eq, Ord, Typeable )
-data Term v s = Var v
- | Node s [ Term v s ]
- deriving Show
+instance Show Identifier where show = name
+mk :: Int -> String -> Identifier
+mk a n = Identifier { arity = a, name = n }
+
+---------------------------------------------------------------------
+
data Rule a = Rule { lhs :: a, rhs :: a
, strict :: Bool
, top :: Bool
}
- deriving Show
+ deriving ( Eq, Ord, Typeable )
data RS s r =
RS { signature :: [ s ] -- ^ better keep order in signature (?)
, rules :: [ Rule r ]
, separate :: Bool -- ^ if True, write comma between rules
}
- deriving Show
+ deriving ( Typeable )
+strict_rules sys =
+ do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
+non_strict_rules sys =
+ do u <- rules sys ; guard $ not $ strict u ; return ( lhs u, rhs u )
+
type TRS v s = RS s ( Term v s )
type SRS s = RS s [ s ]
data Problem v s =
- Problem { trs :: TRS v s
- , strategy :: Strategy
+ Problem { type_ :: Type
+ , trs :: TRS v s
+ , strategy :: Maybe Strategy
-- , metainformation :: Metainformation
- , type_ :: Type
+ , startterm :: Maybe Startterm
}
- deriving Show
data Type = Termination | Complexity
deriving Show
data Strategy = Full | Innermost | Outermost
deriving Show
+
+data Startterm =
+ Startterm_Constructor_based
+ | Startterm_Full
+ deriving Show
+
+------------------------------------------------------
+
+-- | legaca stuff (used in matchbox)
+
+type TES = TRS Identifier Identifier
+type SES = SRS Identifier
+
+mknullary s = Identifier { arity = 0, name = s }
+mkunary s = Identifier { arity = 1, name = s }
+
+from_strict_rules :: Bool -> [(t,t)] -> RS i t
+from_strict_rules sep rs =
+ RS { rules = map ( \ (l,r) ->
+ Rule { strict = True, top = False, lhs = l, rhs = r } ) rs
+ , separate = sep
+ }
+
+with_rules sys rs = sys { rules = rs }
+
+
diff --git a/TPDB/Data/Term.hs b/TPDB/Data/Term.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Data/Term.hs
@@ -0,0 +1,154 @@
+{-# language DeriveDataTypeable #-}
+
+module TPDB.Data.Term where
+
+import qualified Data.Set as S
+import Data.Set (Set)
+import Data.Typeable
+
+data Term v s = Var v
+ | Node s [ Term v s ]
+ deriving ( Eq, Ord, Show, Typeable )
+
+vmap :: ( v -> u ) -> Term v s -> Term u s
+vmap f ( Var v ) = Var ( f v )
+vmap f ( Node c args ) = Node c $ map ( vmap f ) args
+
+instance Functor ( Term v ) where
+ fmap f ( Var v ) = Var v
+ fmap f ( Node c args ) = Node (f c) ( map ( fmap f ) args )
+
+
+
+type Position = [ Int ]
+
+positions :: Term v c
+ -> [ ( Position, Term v c ) ]
+positions t = ( [], t ) : case t of
+ Node c args -> do ( k, arg ) <- zip [ 0 .. ] args
+ ( p, s ) <- positions arg
+ return ( k : p , s )
+ _ -> []
+
+-- | all positions
+pos :: Term v c
+ -> [ Position ]
+pos t = do
+ ( p, s ) <- positions t
+ return p
+
+-- | non-variable positions
+sympos :: Term v c
+ -> [ Position ]
+sympos t = do
+ ( p, Node {} ) <- positions t
+ return p
+
+-- | variable positions
+varpos :: Term v c
+ -> [ Position ]
+varpos t = do
+ ( p, Var {} ) <- positions t
+ return p
+
+-- | leaf positions (= nullary symbols)
+leafpos :: Term v c
+ -> [ Position ]
+leafpos t = do
+ ( p, Node c [] ) <- positions t
+ return p
+
+
+{-# inline subterms #-}
+
+subterms :: Term v c
+ -> [ Term v c ]
+subterms t = t : case t of
+ Node c args -> do arg <- args
+ subterms arg
+ _ -> []
+
+-- | compute new symbol at position, giving the position
+pmap:: ( Position -> c -> d )
+ -> Term v c
+ -> Term v d
+pmap f = rpmap ( \ p c -> f ( reverse p) c )
+
+-- | compute new symbol from *reverse* position and previous symbol
+-- this is more efficient (no reverse needed)
+rpmap :: ( Position -> c -> d )
+ -> Term v c
+ -> Term v d
+rpmap f t = helper [] t where
+ helper p ( Node c args ) = Node ( f p c ) $ do
+ ( k, arg ) <- zip [0..] args
+ return $ helper ( k : p ) arg
+ helper p ( Var v) = Var v
+
+
+
+peek :: Term v c
+ -> Position
+ -> Term v c
+peek t [] = t
+peek ( Node c args ) ( k : ks ) = peek ( args !! k ) ks
+
+peek_symbol :: Term v c
+ -> Position
+ -> c
+peek_symbol t p =
+ case peek t p of
+ Node c args -> c
+ _ -> error "Autolib.TES.Position.peek_symbol called for non-symbol"
+
+-- | warning: don't check arity
+poke_symbol :: Term v c
+ -> ( Position , c )
+ -> Term v c
+poke_symbol t ( p, c ) =
+ case peek t p of
+ Node _ args -> poke t ( p, Node c args )
+ _ -> error "Autolib.TES.Position.poke_symbol called for non-symbol"
+
+poke :: Term v c
+ -> ( Position , Term v c )
+ -> Term v c
+poke t ( [], s ) = s
+poke (Node c args) (k : ks, s ) =
+ let ( pre , this : post ) = splitAt k args
+ in Node c ( pre ++ poke this ( ks, s ) : post )
+
+pokes :: Term v c
+ -> [ ( Position, Term v c ) ]
+ -> Term v c
+pokes = foldl poke
+
+
+-- | in preorder
+symsl :: Term v c -> [ c ]
+symsl t = do
+ Node c _ <- subterms t
+ return c
+
+syms :: Ord c => Term v c -> Set c
+syms = S.fromList . symsl
+
+
+lsyms :: Ord c => Term v c -> [ c ]
+lsyms = S.toList . syms
+
+vars :: Ord v => Term v c -> Set v
+vars t = S.fromList $ do
+ Var v <- subterms t
+ return v
+
+isvar :: Term v c -> Bool
+isvar ( Var _ ) = True ; isvar _ = False
+
+-- | list of variables (each occurs once, unspecified ordering)
+lvars :: Ord v => Term v c -> [ v ]
+lvars = S.toList . vars
+
+-- | list of variables (in pre-order, with duplicates)
+voccs :: Term v c -> [ v ]
+voccs t = do ( p, Var v ) <- positions t ; return v
diff --git a/TPDB/Data/Xml.hs b/TPDB/Data/Xml.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Data/Xml.hs
@@ -0,0 +1,60 @@
+{-# language FlexibleContexts #-}
+{-# language FlexibleInstances #-}
+{-# language UndecidableInstances #-}
+
+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 Data.Typeable
+
+-- | FIXME: move to separate module
+instance XmlContent Identifier where
+ parseContents = do
+ CString _ s _ <- next
+ return $ mknullary s
+ toContents i =
+ -- probably not here: E.xmlEscape E.stdXmlEscaper
+ -- this introduces whitespace between < and =
+ -- [ CString False $ show i ]
+ -- and this creates a CDATA element
+ -- [ CString True $ show i ]
+ -- so here comes an UGLY HACK:
+ [ CString False ( escape $ show i ) () ]
+
+
+instance ( Typeable ( Term v c ) , XmlContent v, XmlContent c )
+ => XmlContent ( Term v c ) where
+ toContents ( Var v ) = rmkel "var" $ toContents v
+{-
+-- for Rainbow:
+ toContents ( Node f xs ) = return $ mkel "app"
+ $ mkel "fun" ( toContents f )
+ : map ( \ x -> mkel "arg" $ toContents x ) xs
+-}
+-- for CPF:
+ toContents ( Node f args ) = rmkel "funapp"
+ $ rmkel "name" ( toContents f )
+ ++ map ( \ arg -> mkel "arg" $ toContents arg ) args
+
+
+
+
+instance HTypeable ( Rule ( Term v c )) where
+ toHType _ = Prim "Rule" "Rule"
+
+instance ( HTypeable ( Rule ( Term v c) )
+ , 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
+ ]
+
+
+
diff --git a/TPDB/Plain/Read.hs b/TPDB/Plain/Read.hs
--- a/TPDB/Plain/Read.hs
+++ b/TPDB/Plain/Read.hs
@@ -12,7 +12,7 @@
import Text.Parsec.Language
import Text.Parsec.Char
import Control.Monad ( guard, void )
-
+import Data.List ( nub )
trs :: String -> Either String ( TRS Identifier Identifier )
trs s = case Text.Parsec.parse reader "input" s of
@@ -41,7 +41,7 @@
instance Reader Identifier where
reader = do
i <- identifier lexer
- return $ Identifier { arity = 0, name = i }
+ return $ Identifier { arity = 0 , name = i }
instance Reader s => Reader [s] where
reader = many reader
@@ -49,11 +49,11 @@
-- NOTE: this is dangerous since we read the variables as constants,
-- and this needs to be patched up later.
-- NOTE: this is more dangerous as we do not set the arity of identifiers
-instance ( Reader v, Reader s ) => Reader ( Term v s ) where
+instance ( Reader v ) => Reader ( Term v Identifier ) where
reader = do
f <- reader
xs <- option [] $ parens lexer $ commaSep lexer reader
- return $ Node f xs
+ return $ Node ( f { arity = length xs } ) xs
instance Reader u => Reader ( Rule u ) where
reader = do
@@ -105,18 +105,26 @@
ds <- many $ declaration False
return $ make_trs ds
-make_srs :: [ Declaration [s] ] -> SRS s
-make_srs ds =
- let us = do Rules_Declaration us <- ds ; us
- in RS { signature = [] , rules = us, separate = True }
+repair_signature_srs sys =
+ let sig = nub $ do u <- rules sys ; lhs u ++ rhs u
+ in sys { signature = sig }
+make_srs :: Eq s => [ Declaration [s] ] -> SRS s
+make_srs ds = repair_signature_srs $
+ let us = do Rules_Declaration us <- ds ; us
+ in RS { rules = us, separate = True }
+
+repair_signature_trs sys =
+ let sig = nub $ do u <- rules sys ; lsyms ( lhs u ) ++ lsyms ( rhs u)
+ in sys { signature = sig }
+
make_trs :: [ Declaration ( Term Identifier Identifier ) ]
-> TRS Identifier Identifier
-make_trs ds =
+make_trs ds = repair_signature_trs $
let vs = do Var_Declaration vs <- ds ; vs
us = do Rules_Declaration us <- ds ; us
us' = repair_variables vs us
- in RS { signature = [], rules = us', separate = False }
+ in RS { rules = us', separate = False }
repair_variables vars rules = do
diff --git a/TPDB/Plain/Write.hs b/TPDB/Plain/Write.hs
--- a/TPDB/Plain/Write.hs
+++ b/TPDB/Plain/Write.hs
@@ -6,11 +6,9 @@
module TPDB.Plain.Write where
import TPDB.Data
-
+import TPDB.Pretty
import Text.PrettyPrint.HughesPJ
-class Pretty a where pretty :: a -> Doc
-
instance Pretty Identifier where
pretty i = text $ name i
@@ -21,17 +19,22 @@
[] -> pretty f
_ -> pretty f <+> parens ( fsep $ punctuate comma $ map pretty xs )
-instance Pretty a => Pretty ( Rule a ) where
- pretty u = hsep [ pretty $ lhs u
+instance PrettyTerm a => Pretty ( Rule a ) where
+ pretty u = hsep [ prettyTerm $ lhs u
, if strict u then text "->" else text "->="
-- FIXME: implement "top" annotation
- , pretty $ rhs u
+ , prettyTerm $ rhs u
]
-instance Pretty s => Pretty [s] where
- pretty xs = hsep $ map pretty xs
+class PrettyTerm a where prettyTerm :: a -> Doc
-instance ( Pretty s, Pretty r ) => Pretty ( RS s r ) where
+instance Pretty s => PrettyTerm [s] where
+ prettyTerm xs = hsep $ map pretty xs
+
+instance ( Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where
+ prettyTerm = pretty
+
+instance ( Pretty s, PrettyTerm r ) => Pretty ( RS s r ) where
pretty sys = vcat
[ parens $ text "RULES" <+>
vcat ( ( if separate sys then punctuate comma else id )
@@ -41,4 +44,12 @@
]
instance ( Pretty s, Pretty r ) => Pretty ( Problem s r ) where
- pretty p = pretty $ trs p
+ pretty p = vcat
+ [ pretty $ trs p
+ , case strategy p of
+ Nothing -> empty
+ Just s -> fsep [ text "strategy", text ( show s ) ]
+ , case startterm p of
+ Nothing -> empty
+ Just s -> fsep [ text "startterm", text ( show s ) ]
+ ]
diff --git a/TPDB/Pretty.hs b/TPDB/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Pretty.hs
@@ -0,0 +1,13 @@
+module TPDB.Pretty where
+
+import Text.PrettyPrint.HughesPJ
+
+class Pretty a where pretty :: a -> Doc
+
+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 [a] where
+ pretty xs = brackets $ fsep $ punctuate comma $ map pretty xs
diff --git a/TPDB/Rainbow/Proof/Type.hs b/TPDB/Rainbow/Proof/Type.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Rainbow/Proof/Type.hs
@@ -0,0 +1,158 @@
+{-# OPTIONS -fglasgow-exts #-}
+
+-- | internal representation of Rainbow termination proofs,
+-- see
+-- this file is modelled after rainbow/proof.ml
+-- it omits constructors not needed for matrix interpretations (for the moment)
+module TPDB.Rainbow.Proof.Type
+
+where
+
+import TPDB.Data hiding ( Type (..))
+import TPDB.Pretty
+import TPDB.Plain.Write () -- just instances
+import Text.PrettyPrint.HughesPJ
+
+import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
+import qualified Text.Parsec as P
+
+import qualified Data.Time as T
+import Data.Typeable
+
+data Vector a = Vector [ a ]
+ deriving Typeable
+
+data Matrix a = Matrix [ Vector a ]
+ deriving Typeable
+
+data MaxPlus = MinusInfinite | Finite Integer
+ deriving ( Show, Read, Typeable )
+
+data Mi_Fun a =
+ Mi_Fun { mi_const :: Vector a
+ , mi_args :: [ Matrix a ]
+ }
+ deriving Typeable
+
+data Poly_Fun a =
+ Poly_Fun { coefficients :: [a]
+ }
+ deriving Typeable
+
+type Matrix_Int = Interpretation Mi_Fun
+type Polynomial_Int = Interpretation Poly_Fun
+
+data Interpretation f = forall k a
+ . ( XmlContent k, XmlContent a, Typeable a ) -- Haskell2Xml a
+ =>
+ Interpretation { mi_domain :: Domain
+ , mi_dim :: Integer
+ , mi_duration :: T.NominalDiffTime -- ^ this is an extension
+ , mi_start :: T.UTCTime
+ , mi_end :: T.UTCTime
+ -- , mi_int :: [ (k , Mi_Fun a ) ]
+ , mi_int :: [ (k , f a ) ]
+ }
+
+instance Typeable (Interpretation f )
+
+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
+
+data Red_Ord
+ = Red_Ord_Matrix_Int Matrix_Int
+ | Red_Ord_Polynomial_Int Polynomial_Int
+ | Red_Ord_Simple_Projection Simple_Projection
+ | Red_Ord_Usable_Rules Usable_Rules
+ deriving Typeable
+
+data Usable_Rules = Usable_Rules [ Identifier ]
+ deriving Typeable
+
+instance Pretty Usable_Rules where
+ pretty (Usable_Rules sp) = text "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
+
+data Claim =
+ Claim { system :: TRS Identifier Identifier
+ , property :: Property
+ }
+ deriving Typeable
+
+data Proof =
+ Proof { claim :: Claim
+ , reason :: Reason
+ }
+ deriving Typeable
+
+data Property
+ = Termination
+ | Top_Termination
+ | Complexity ( Function, Function )
+ deriving ( Typeable )
+
+instance Show Property where show = render . pretty
+
+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 )
+
+-- | see specification:
+-- http://termination-portal.org/wiki/Complexity
+data Function
+ = Unknown
+ | Polynomial { degree :: Maybe Int }
+ | Exponential
+ deriving ( Typeable )
+
+instance Show Function where show = render . pretty
+
+instance Pretty Function where
+ pretty f = case f of
+ Unknown -> text "?"
+ Polynomial { degree = Nothing } ->
+ text "POLY"
+ Polynomial { degree = Just 0 } ->
+ text "O(1)"
+ Polynomial { degree = Just d } ->
+ text "O" <+> parens ( text "n^" <> pretty d)
+
+
+
+data Reason
+ = Trivial
+ | MannaNess Red_Ord Proof
+ | MarkSymb Proof
+ | DP Proof
+ | Reverse Proof
+ | As_TRS Proof
+ | As_SRS Proof
+ | SCC [ Proof ] -- ^ proposed extension
+ | RFC Proof -- ^ experimental (not in Rainbow)
+ | Undo_RFC Proof -- ^ experimental (not in Rainbow)
+ | Bounded_Matrix_Interpretation Proof -- ^ TODO add more info
+ deriving Typeable
+
+data Over_Graph = HDE | HDE_Marked
+ deriving ( Show, Typeable )
+
+data Marked a = Hd_Mark a | Int_Mark a
+ deriving ( Eq, Ord, Typeable )
+
+
+
+
+
+
diff --git a/TPDB/Rainbow/Proof/Xml.hs b/TPDB/Rainbow/Proof/Xml.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Rainbow/Proof/Xml.hs
@@ -0,0 +1,285 @@
+{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}
+
+-- | from internal representation to XML, and back
+
+module TPDB.Rainbow.Proof.Xml where
+
+import TPDB.Rainbow.Proof.Type
+
+import TPDB.Xml
+import TPDB.Data.Xml
+-- import Matrix.MaxPlus ( MaxPlus )
+-- import Autolib.Reader hiding ( many )
+-- import Autolib.TES
+-- import Autolib.TES.Identifier ( mk, mknullary, mkunary )
+
+import TPDB.Data
+
+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(..) )
+
+import Data.List ( nub )
+import Data.Char ( toLower )
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import qualified Data.Time as T
+import Control.Monad
+import Data.Typeable
+
+tox :: Proof -> Document ()
+tox p =
+ let xd = XMLDecl "1.0" ( Just $ EncodingDecl "ISO-8859-1" ) Nothing
+ pro = Prolog ( Just xd ) [] Nothing []
+ t = toplevel p
+ et = E.xmlEscape E.stdXmlEscaper t
+ -- don't escape, see remarks in Autolib.TES.Identifier
+ in Document pro emptyST t []
+
+
+toplevel p =
+ let atts = [ ( N "xmlns"
+ , AttValue [ Left "urn:rainbow.proof.format" ]
+ )
+ , ( N "xmlns:xsi"
+ , AttValue [ Left "http://www.w3.org/2001/XMLSchema-instance" ]
+ )
+ , ( N "xsi:schemaLocation"
+ , AttValue [ Left "urn:rainbow.proof.format http://color.loria.fr/proof.xsd" ]
+ )
+ ]
+ unProof [ CElem ( Elem (N "proof") [] cs ) _ ] = cs
+ in Elem (N "proof") atts $ unProof $ toContents p
+
+
+instance ( Typeable a, XmlContent a ) => XmlContent ( Vector a ) where
+ toContents ( Vector xs ) =
+ map ( \ x -> mkel "velem" ( toContents x ) ) xs
+ parseContents = wrap xread
+
+instance XRead a => XRead ( Vector a ) where
+ xread = fmap Vector $ many $ element "velem" xread
+
+
+-- FIXME:
+instance XmlContent MaxPlus where
+ parseContents = do
+ CString _ s _ <- next
+ return $ read s
+ toContents i =
+ [ CString False ( escape $ show i ) () ]
+
+
+-- | for some types, e.g. Integer
+-- , do not use XmlContent instance for element type
+-- but show them (as string).
+-- reason: the XmlContent module contains an instance
+-- for integer that produces
+-- and there is no way to turn this off.
+
+data Xml_As_String a = Xml_As_String a
+ deriving Typeable
+
+instance ( Typeable a, Show a, Read a ) => XmlContent (Xml_As_String a) where
+ toContents ( Xml_As_String x ) = [ CString False ( show x ) () ]
+ parseContents = wrap $ fmap Xml_As_String $ xfromstring
+
+instance ( Typeable a, XmlContent a )
+ => XmlContent ( Matrix a ) where
+ toContents ( Matrix xs ) =
+ map ( \ x -> mkel "row" ( toContents x ) ) xs
+ parseContents = wrap xread
+
+instance XRead a => XRead ( Matrix a ) where
+ xread = do
+ rs <- many $ element "row" xread
+ return $ Matrix rs
+
+instance ( Typeable a, XmlContent a )
+ => XmlContent ( Mi_Fun a ) where
+ toContents ( Mi_Fun { mi_const = c, mi_args = xs } ) = return $
+ mkel "mi_fun"
+ $ mkel "const" ( toContents c )
+ : map ( mkel "arg" . toContents ) xs
+ parseContents = wrap xread
+
+instance XRead a => XRead ( Mi_Fun a ) where
+ xread = element "mi_fun" $ do
+ con <- element "const" xread
+ args <- many $ element "arg" xread
+ return $ Mi_Fun { mi_const = con, mi_args = args }
+
+
+
+--------------------------------------------------------------------------------
+
+instance XmlContent Domain where
+ toContents d = [ CString False ( show d ) ( )]
+
+instance XmlContent Matrix_Int where
+ toContents ( Interpretation { mi_domain = o, mi_dim = d, mi_int = i
+ , mi_start = s, mi_end = e, mi_duration = u } ) =
+ return $ mkel ( case o of Natural -> "matrix_int"
+ Arctic -> "arctic_int"
+ Arctic_Below_Zero -> "arctic_bz_int"
+ Tropical -> "tropical_int" )
+ [ mkel "dimension" [ CString False ( show d ) () ]
+ , mkel "mi_map" $ do
+ ( k, v ) <- i
+ return $ mkel "mapping"
+ $ mkel "fun" ( toContents k )
+ : toContents v
+ -- the following are not standard rainbow,
+ -- so they have to come after the standard elements
+ -- because the rainbow parser then ignores them
+ , mkel "start" [ CString False ( show s ) () ]
+ , mkel "end" [ CString False ( show e ) () ]
+ , mkel "duration" [ CString False ( show u ) () ]
+ ]
+ parseContents = wrap xread
+
+instance XRead Matrix_Int where
+ xread = foldr1 orelse
+ [ mai "matrix_int" Natural ( undefined :: Xml_As_String Integer )
+ , mai "arctic_int" Arctic ( undefined :: MaxPlus )
+ , mai "arctic_bz_int" Arctic_Below_Zero ( undefined :: MaxPlus )
+ ]
+
+-- | FIXME this is broken because the keys could be
+-- Identifier or Marked Identifier
+mai :: forall a . ( Typeable a, XmlContent a )
+ => String -> Domain -> a -> CParser Matrix_Int
+mai tag o v0 = element tag $ do
+ d <- element "dimension" $ xfromstring
+ i <- element "mi_map" $ many $ element "mapping" $ do
+ k :: Identifier <- element "fun" $ xread -- FIXME
+ v :: Mi_Fun a <- xread
+ return ( k, v )
+ s <- element "start" $ xfromstring
+ e <- element "end" $ xfromstring
+ let u = T.diffUTCTime e s
+ return $ Interpretation
+ { mi_domain = o, mi_dim = d, mi_int = i
+ , mi_start = s, mi_end = e, mi_duration = u
+ }
+
+instance XmlContent Red_Ord where
+ toContents ro = case ro of
+ Red_Ord_Matrix_Int mi -> return $
+ mkel "order" $ toContents mi
+ Red_Ord_Simple_Projection sp -> return $
+ mkel "order" $ toContents sp
+ parseContents = wrap xread
+
+instance XmlContent Simple_Projection where
+ toContents ( Simple_Projection sp ) = return $
+ mkel "simple_projection" $ map ( \ (f,i) ->
+ mkel "project" [ mkel "symbol" $ toContents (Hd_Mark $ unP f)
+ , mkel "position" $ toContents $ Xml_As_String i
+ ]
+ ) sp
+ parseContents = wrap xread
+
+instance XRead Simple_Projection where
+ xread = element "simple_projection"
+ $ fmap Simple_Projection xread
+
+instance XRead Red_Ord where
+ xread = element "order"
+ $ orelse ( fmap Red_Ord_Matrix_Int xread )
+ ( fmap Red_Ord_Simple_Projection xread )
+
+instance HTypeable Proof where
+ toHType p = Prim "proof" "proof"
+
+
+instance XmlContent Proof where
+ toContents p0 = let { p = reason p0 } in return $ mkel "proof" $ case p of
+ Trivial -> return $ mkel "trivial" []
+ MannaNess o p -> return
+ $ mkel "manna_ness" $ toContents o ++ toContents p
+ MarkSymb p -> return $ mkel "mark_symbols" $ toContents p
+ DP p -> return $ mkel "dp" $ toContents p
+ As_TRS p -> return $ mkel "as_trs" $ toContents p
+ Reverse p -> return $ mkel "reverse" $ toContents p
+ SCC parts -> return $ mkel "scc_decomp"
+ $ mkel "graph" ( toContents HDE_Marked )
+ : do
+ p <- parts
+ let sys = system $ claim p
+ vs = signature sys
+ u = head $ filter strict $ rules sys
+ return $ mkel "scc"
+ $ toContents ( externalize vs u )
+ ++ toContents p
+ parseContents = wrap xread
+
+instance XRead Proof where
+ xread = element "proof" $ do
+ let cl = undefined
+ rs <- foldr1 orelse
+ [ element "trivial" $ return Trivial
+ , element "reverse" $ fmap Reverse xread
+ , element "as_trs" $ fmap As_TRS xread
+ , element "manna_ness" $ do return () ; o <- xread ; p <- xread ; return $ MannaNess o p
+ , element "mark_symbols" $ fmap MarkSymb xread
+ , element "dp" $ fmap DP xread
+ , complain "Proof"
+ ]
+ return $ Proof { claim = cl, reason = rs }
+
+externalize :: [ Identifier ]
+ -> Rule ( Term Identifier Identifier )
+ -> Rule ( Term Identifier ( Marked Identifier ) )
+externalize vs u =
+ let -- HACK: rainbow/DPSCC requires variables be numbered
+ -- according to inverse order in declaration (!?)
+ m = Map.fromList
+ $ zip ( reverse vs )
+ $ map ( \ i -> mknullary $ "v" ++ show i ) [ 1 .. ]
+ rename :: Identifier -> Identifier
+ rename v = let Just w = Map.lookup v m in w
+ handle ( Node f args ) = Node ( Hd_Mark $ unP f )
+ $ map ( fmap Int_Mark . vmap rename ) args
+ in Rule { lhs = handle $ lhs u, rhs = handle $ rhs u, strict = True , top = False }
+
+-- | super ugly risky: name mangling
+unP :: Identifier -> Identifier
+unP k = let cs = show k
+ in case last cs of 'P' -> mknullary $ init cs
+
+instance XmlContent Over_Graph where
+ toContents og = return $ mkel ( map toLower $ show og ) []
+
+instance ( Typeable a, XmlContent a ) => XmlContent ( Marked a ) where
+ toContents m = case m of
+{-
+ Hd_Mark x -> return $ mkel "hd_mark" $ toContents x
+ Int_Mark x -> return $ mkel "int_mark" $ toContents x
+-}
+-- HACK
+ Hd_Mark x -> rmkel "sharp" $ rmkel "name" $ toContents x
+ Int_Mark x -> rmkel "name" $ toContents x
+
+ parseContents = wrap xread
+
+instance ( Typeable a, XmlContent a ) => XRead ( Marked a ) where
+ xread = foldr1 orelse
+ [ fmap Hd_Mark $ element "hd_mark" xread
+ , fmap Int_Mark $ element "int_mark" xread
+ , complain "Marked"
+ ]
+
+-- FIXME
+instance XRead Identifier where
+ xread = CParser $ \ ( c : cs ) ->
+ return ( mknullary "some_identifier" , cs )
+ -- error $ info [c]
+
+-- FIXME: we will need this for SCC
+-- instance XmlContent TES where
+
diff --git a/TPDB/XTC/Read.hs b/TPDB/XTC/Read.hs
--- a/TPDB/XTC/Read.hs
+++ b/TPDB/XTC/Read.hs
@@ -25,13 +25,13 @@
getVar = proc x -> do
nm <- getText <<< getChildren <<< hasName "var" -< x
- returnA -< Var $ Identifier { arity = 0, name = nm }
+ returnA -< Var $ Identifier { name = nm, arity = 0 }
getFunApp = proc x -> do
sub <- hasName "funapp" -< x
nm <- getText <<< gotoChild "name" -< sub
gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub
- let c = Identifier { arity = length gs , name = nm }
+ let c = Identifier { name = nm, arity = length gs }
returnA -< Node c gs
gotoChild tag = proc x -> do
@@ -44,12 +44,14 @@
ty <- getType <<< getAttrValue "type" -< x
rs <- getTRS <<< getChild "trs" -< x
st <- getStrategy <<< getChild "strategy" -< x
- returnA -< case st of
- Full -> Problem { trs = rs
+ stt <- listA ( getStartterm <<< getChild "startterm" ) -< x
+ returnA -< Problem { trs = rs
, TPDB.Data.strategy = st
, type_ = ty
+ , startterm = case stt of
+ [] -> Nothing
+ [x] -> x
}
- _ -> error $ unwords [ "cannot handle strategy", show st ]
getType = proc x -> do
returnA -< case x of
@@ -59,8 +61,16 @@
getStrategy = proc x -> do
cs <- getText <<< getChildren -< x
returnA -< case cs of
- "FULL" -> Full
+ "FULL" -> Just Full
+getStartterm = ( proc x -> do
+ getChild "constructor-based" -< x
+ returnA -< Just Startterm_Constructor_based
+ ) <+> ( proc x -> do
+ getChild "full" -< x
+ returnA -< Just Startterm_Full
+ ) <+> ( proc x -> do returnA -< Nothing )
+
getTRS = proc x -> do
sig <- getSignature <<< getChild "signature" -< x
str <- getRules True <<< getChild "rules" -< x
@@ -80,7 +90,7 @@
getFuncsym = proc x -> do
nm <- getText <<< gotoChild "name" -< x
ar <- getText <<< gotoChild "arity" -< x
- returnA -< Identifier { arity = read ar, name = nm }
+ returnA -< Identifier { name = nm , arity = read ar }
getRules str = proc x -> do
returnA <<< listA ( getRule str <<< getChild "rule" ) -< x
diff --git a/TPDB/Xml.hs b/TPDB/Xml.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/Xml.hs
@@ -0,0 +1,107 @@
+{-# language UndecidableInstances, OverlappingInstances, IncoherentInstances, FlexibleInstances, ScopedTypeVariables #-}
+
+module TPDB.Xml where
+
+import Text.XML.HaXml.Types (QName (..) )
+import Text.XML.HaXml.XmlContent.Haskell
+import Text.XML.HaXml.Posn ( Posn )
+
+import qualified Text.XML.HaXml.Pretty as P
+
+import Data.Typeable
+
+mkel name cs = CElem ( Elem (N name) [] cs ) ()
+rmkel name cs = return $ mkel name cs
+
+instance Typeable t => HTypeable t where
+ toHType x = let cs = show ( typeOf x ) in Prim cs cs
+
+escape [] = []
+escape ( c : cs ) = case c of
+ '<' -> "<" ++ escape cs
+ '>' -> ">" ++ escape cs
+ _ -> c : escape cs
+
+
+type Contents = [ Content Posn ]
+
+data CParser a = CParser { unCParser :: Contents -> Maybe ( a, Contents ) }
+
+instance Functor CParser where
+ fmap f (CParser p) = CParser $ \ cs ->
+ do ( x, cs' ) <- p cs ; return ( f x, cs' )
+
+instance Monad CParser where
+ return x = CParser $ \ cs -> return ( x, cs )
+ CParser p >>= f = CParser $ \ cs0 ->
+ do ( x, cs1 ) <- p cs0 ; unCParser ( must_succeed $ f x ) cs1
+
+
+must_succeed :: CParser a -> CParser a
+must_succeed (CParser p ) = CParser $ \ cs ->
+ case p cs of
+ Nothing -> error $ "must succeed:" ++ errmsg cs
+ ok -> ok
+
+class Typeable a => XRead a where xread :: CParser a
+
+
+instance ( Typeable a, XmlContent a ) => XRead a where
+ xread = CParser $ \ cs -> case runParser parseContents cs of
+ ( Right x, rest ) -> Just ( x, rest )
+ ( Left err, rest ) -> Nothing
+
+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
+ : []
+ Just ( x, cs' ) -> Committed ( Success cs' x )
+
+errmsg cs = unlines $ case cs of
+ ( c : etc ) ->
+ [ show $ P.content c
+
+ ]
+ _ -> [ show $ length cs ]
+
+orelse :: CParser a -> CParser a -> CParser a
+orelse ( CParser p ) ( CParser q ) = CParser $ \ cs ->
+ case p cs of Nothing -> q cs ; ok -> ok
+
+many :: CParser a -> CParser [a]
+many p = ( do x <- p ; xs <- TPDB.Xml.many p ; return $ x : xs ) `orelse` return []
+
+element tag p = element0 (N tag) $ must_succeed p
+
+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
+
+strip [] = []
+strip input @ ( CElem ( Elem {} ) _ : _ ) = input
+strip (c : cs) = strip cs
+
+xfromstring :: Read a => CParser a
+xfromstring = CParser $ \ cs -> case cs of
+ ( CString _ s _ : etc ) -> Just ( read s, etc )
+ _ -> Nothing
+
+complain :: String -> CParser a
+complain tag = CParser $ \ cs -> error $ "ERROR: in branch for " ++ tag ++ errmsg cs
+
+info :: Contents -> String
+info [] = "empty contents"
+info ( c : cs ) = case c of
+ CElem ( Elem name atts con ) _ -> "CElem, name: " ++ show name
+ CString _ s _ -> "CString : " ++ s
+ CRef _ _ -> "CRef"
+ CMisc _ _ -> "CMisc"
+
+
+
diff --git a/test/read_print_srs.hs b/test/read_print_srs.hs
--- a/test/read_print_srs.hs
+++ b/test/read_print_srs.hs
@@ -1,5 +1,6 @@
import TPDB.Plain.Write
import TPDB.Plain.Read
+import TPDB.Pretty
import Control.Monad ( forM, void )
diff --git a/test/read_print_trs.hs b/test/read_print_trs.hs
--- a/test/read_print_trs.hs
+++ b/test/read_print_trs.hs
@@ -1,5 +1,6 @@
import TPDB.Plain.Write
import TPDB.Plain.Read
+import TPDB.Pretty
import Control.Monad ( forM, void )
diff --git a/test/read_print_xml.hs b/test/read_print_xml.hs
--- a/test/read_print_xml.hs
+++ b/test/read_print_xml.hs
@@ -1,12 +1,10 @@
-
import TPDB.Data
-
+import TPDB.Pretty
import TPDB.XTC
import TPDB.Plain.Write
import Control.Monad ( forM, void )
main = void $ do
- ps <- readProblems "test/3.15.xml"
- print $ length ps
- forM ps ( print . pretty )
+ [ p ] <- readProblems "test/3.15.xml"
+ print $ pretty p
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
Name: tpdb
-Version: 0.1
+Version: 0.3
Author: Johannes Waldmann
Maintainer: Johannes Waldmann
Category: Science
@@ -10,7 +10,8 @@
Description:
- The package defines data types and parsers for rewriting systems,
+ The package defines data types and parsers for rewriting systems
+ and termination proofs,
as used in the Termination Competitions.
For syntax and semantics specification,
see
@@ -25,27 +26,32 @@
-- test/3.15.xml, test/33.trs , test/z001.srs
Library
- Build-Depends: base==4.*, hxt, pretty, parsec
+ Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml
Exposed-Modules:
- TPDB.Data,
- TPDB.Plain.Write, TPDB.Plain.Read,
- TPDB.XTC, TPDB.XTC.Read
-
+ TPDB.Data, TPDB.Data.Term, TPDB.Data.Xml
+ TPDB.Pretty, TPDB.Plain.Write, TPDB.Plain.Read,
+ TPDB.XTC, TPDB.XTC.Read, TPDB.Xml,
+ TPDB.Rainbow.Proof.Xml, TPDB.Rainbow.Proof.Type
+ TPDB.CPF.Proof.Xml, TPDB.CPF.Proof.Type
Test-Suite XML
+ Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml
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, HaXml
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, HaXml
Type: exitcode-stdio-1.0
main-is: read_print_srs.hs
+
hs-source-dirs: test .