tpdb 0.1 → 0.3
raw patch · 16 files changed
+1150/−50 lines, 16 filesdep +HaXmldep +containersdep +time
Dependencies added: HaXml, containers, time
Files
- TPDB/CPF/Proof/Type.hs +105/−0
- TPDB/CPF/Proof/Xml.hs +134/−0
- TPDB/Data.hs +60/−11
- TPDB/Data/Term.hs +154/−0
- TPDB/Data/Xml.hs +60/−0
- TPDB/Plain/Read.hs +18/−10
- TPDB/Plain/Write.hs +21/−10
- TPDB/Pretty.hs +13/−0
- TPDB/Rainbow/Proof/Type.hs +158/−0
- TPDB/Rainbow/Proof/Xml.hs +285/−0
- TPDB/XTC/Read.hs +17/−7
- TPDB/Xml.hs +107/−0
- test/read_print_srs.hs +1/−0
- test/read_print_trs.hs +1/−0
- test/read_print_xml.hs +3/−5
- tpdb.cabal +13/−7
+ TPDB/CPF/Proof/Type.hs view
@@ -0,0 +1,105 @@+{-# OPTIONS -fglasgow-exts #-}++-- | internal representation of CPF termination proofs,+-- see <http://cl-informatik.uibk.ac.at/software/cpf/>++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 )++++++++
+ TPDB/CPF/Proof/Xml.hs view
@@ -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++++++
TPDB/Data.hs view
@@ -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 }++
+ TPDB/Data/Term.hs view
@@ -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
+ TPDB/Data/Xml.hs view
@@ -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+ ]+++
TPDB/Plain/Read.hs view
@@ -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
TPDB/Plain/Write.hs view
@@ -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 ) ] + ]
+ TPDB/Pretty.hs view
@@ -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
+ TPDB/Rainbow/Proof/Type.hs view
@@ -0,0 +1,158 @@+{-# OPTIONS -fglasgow-exts #-}++-- | internal representation of Rainbow termination proofs,+-- see <http://color.loria.fr/>+-- 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 )++++++
+ TPDB/Rainbow/Proof/Xml.hs view
@@ -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 <integer value="42"/>+-- 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+
TPDB/XTC/Read.hs view
@@ -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
+ TPDB/Xml.hs view
@@ -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"+++
test/read_print_srs.hs view
@@ -1,5 +1,6 @@ import TPDB.Plain.Write import TPDB.Plain.Read+import TPDB.Pretty import Control.Monad ( forM, void )
test/read_print_trs.hs view
@@ -1,5 +1,6 @@ import TPDB.Plain.Write import TPDB.Plain.Read+import TPDB.Pretty import Control.Monad ( forM, void )
test/read_print_xml.hs view
@@ -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
tpdb.cabal view
@@ -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 <http://www.termination-portal.org/wiki/TPDB>@@ -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 .