From baf5f3e73864c92cc85566a1ac4d3b583c326cbe Mon Sep 17 00:00:00 2001 From: Johannes Waldmann Date: Thu, 17 Jul 2014 18:54:12 +0200 Subject: [PATCH] issue #12 --- TPDB/CPF/Proof/Read.hs | 14 ++++---- TPDB/CPF/Proof/Type.hs | 74 +++++++++++++++++++++++------------------ TPDB/CPF/Proof/Write.hs | 10 ++++-- tpdb.cabal | 2 +- 4 files changed, 59 insertions(+), 41 deletions(-) diff --git a/TPDB/CPF/Proof/Read.hs b/TPDB/CPF/Proof/Read.hs index 71e50ad..f76f9f2 100644 --- a/TPDB/CPF/Proof/Read.hs +++ b/TPDB/CPF/Proof/Read.hs @@ -32,19 +32,20 @@ readCP = readCP_with_tracelevel 0 readCP_with_tracelevel l s = runX ( X.withTraceLevel l $ readString [] s >>> getCP ) -getCP = atTag "certificationProblem" >>> proc x -> do +getCP = getChild "certificationProblem" >>> proc x -> do inp <- getInput <<< getChild "input" -< x pro <- getProof <<< getChild "proof" -< x ver <- getText <<< gotoChild "cpfVersion" -< x - returnA -< CertificationProblem { input = inp, proof = pro, cpfVersion = "2.2" } + returnA -< CertificationProblem + { input = inp, proof = pro, cpfVersion = ver, origin = ignoredOrigin } getInput = getTerminationInput <+> getComplexityInput -getTerminationInput = atTag "input" >>> proc x -> do +getTerminationInput = hasName "input" >>> proc x -> do trsI <- getTrsInput <<< getChild "trsInput" -< x returnA -< TrsInput $ RS { rules = trsI, separate = False } -getComplexityInput = atTag "input" >>> proc x -> do +getComplexityInput = hasName "input" >>> proc x -> do y <- getChild "complexityInput" -< x trsI <- getTrsInput <<< getChild "trsInput" -< y cm <- getComplexityMeasure -< y @@ -80,7 +81,8 @@ getProof = getDummy "trsTerminationProof" ( TrsTerminationProof undefined ) <+> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined ) <+> getDummy "complexityProof" ( ComplexityProof undefined ) -getDummy t c = atTag t >>> proc x -> do +getDummy t c = proc x -> do + getChild t -< x returnA -< c getRules str = proc x -> do @@ -111,5 +113,5 @@ gotoChild tag = proc x -> do getChild tag = proc x -> do returnA <<< hasName tag <<< isElem <<< getChildren -< x -atTag tag = deep (isElem >>> hasName tag) + diff --git a/TPDB/CPF/Proof/Type.hs b/TPDB/CPF/Proof/Type.hs index fb2c89e..083f74c 100644 --- a/TPDB/CPF/Proof/Type.hs +++ b/TPDB/CPF/Proof/Type.hs @@ -1,4 +1,6 @@ -{-# OPTIONS -fglasgow-exts #-} +{-# language StandaloneDeriving #-} +{-# language ExistentialQuantification #-} +{-# language DeriveDataTypeable #-} -- | internal representation of CPF termination proofs, -- see @@ -23,12 +25,17 @@ data CertificationProblem = , proof :: Proof , origin :: Origin } - deriving ( Typeable ) + deriving ( Typeable, Eq ) + +data Origin = ProofOrigin { tool :: Tool } + deriving ( Typeable, Eq ) -data Origin = ProofOrigin Tool - deriving Typeable -data Tool = Tool { name :: String , version :: String } - deriving Typeable +ignoredOrigin = ProofOrigin { tool = Tool "ignored" "ignored" } + +data Tool = Tool { name :: String + , version :: String + } + deriving ( Typeable, Eq ) data CertificationProblemInput = TrsInput { trsinput_trs :: TRS Identifier Identifier } @@ -39,38 +46,39 @@ data CertificationProblemInput , complexityMeasure :: ComplexityMeasure , complexityClass :: ComplexityClass } - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Proof = TrsTerminationProof TrsTerminationProof | TrsNonterminationProof TrsNonterminationProof | RelativeTerminationProof TrsTerminationProof | RelativeNonterminationProof TrsNonterminationProof | ComplexityProof ComplexityProof - deriving ( Typeable ) + deriving ( Typeable, Eq ) -data DPS = forall s . ( XmlContent s , Typeable s ) +data DPS = forall s . ( XmlContent s , Typeable s, Eq s ) => DPS [ Rule (Term Identifier s) ] deriving ( Typeable ) +instance Eq DPS where x == y = error "instance Eq DPS" data ComplexityProof = ComplexityProofFIXME () - deriving ( Typeable ) + deriving ( Typeable, Eq ) data ComplexityMeasure = DerivationalComplexity | RuntimeComplexity - deriving ( Typeable ) + deriving ( Typeable, Eq ) data ComplexityClass = ComplexityClassPolynomial { degree :: Int } -- ^ it seems the degree must always be given in CPF, -- although the category spec also allows "POLY" -- http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php - deriving ( Eq, Typeable ) + deriving ( Typeable, Eq ) data TrsNonterminationProof = TrsNonterminationProofFIXME () - deriving ( Typeable ) + deriving ( Typeable, Eq ) data TrsTerminationProof = RIsEmpty @@ -90,10 +98,10 @@ data TrsTerminationProof | StringReversal { trs :: TRS Identifier Identifier , trsTerminationProof :: TrsTerminationProof } - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Model = FiniteModel Int [Interpret] - deriving ( Typeable ) + deriving ( Typeable, Eq ) data DpProof = PIsEmpty | RedPairProc { rppOrderingConstraintProof :: OrderingConstraintProof @@ -112,53 +120,53 @@ data DpProof = PIsEmpty , ulpTrs :: DPS , ulpDpProof :: DpProof } - deriving ( Typeable ) + deriving ( Typeable, Eq ) data DepGraphComponent = DepGraphComponent { dgcRealScc :: Bool , dgcDps :: DPS , dgcDpProof :: DpProof } - deriving ( Typeable ) + deriving ( Typeable, Eq ) data OrderingConstraintProof = OCPRedPair RedPair - deriving ( Typeable ) + deriving ( Typeable, Eq ) data RedPair = RPInterpretation Interpretation | RPPathOrder PathOrder - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Interpretation = Interpretation { interpretation_type :: Interpretation_Type , interprets :: [ Interpret ] } - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Interpretation_Type = Matrix_Interpretation { domain :: Domain, dimension :: Int , strictDimension :: Int } - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Domain = Naturals | Rationals Rational | Arctic Domain | Tropical Domain - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Interpret = Interpret { symbol :: Symbol , arity :: Int , value :: Value } - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Value = Polynomial Polynomial | ArithFunction ArithFunction - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Polynomial = Sum [ Polynomial ] | Product [ Polynomial ] | Polynomial_Coefficient Coefficient | Polynomial_Variable String - deriving ( Typeable ) + deriving ( Typeable, Eq ) data ArithFunction = AFNatural Integer | AFVariable Integer @@ -167,39 +175,41 @@ data ArithFunction = AFNatural Integer | AFMin [ArithFunction] | AFMax [ArithFunction] | AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Symbol = SymName Identifier | SymSharp Symbol | SymLabel Symbol Label - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Label = LblNumber [Integer] | LblSymbol [Symbol] - deriving ( Typeable ) + deriving ( Typeable, Eq ) data Coefficient = Vector [ Coefficient ] | Matrix [ Coefficient ] - | forall a . XmlContent a => Coefficient_Coefficient a + | forall a . (Eq a, XmlContent a ) => Coefficient_Coefficient a deriving ( Typeable ) +instance Eq Coefficient where x == y = error "instance Eq Coefficient" + data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite deriving Typeable class ToExotic a where toExotic :: a -> Exotic data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry] - deriving Typeable + deriving ( Typeable, Eq ) data PrecedenceEntry = PrecedenceEntry { peSymbol :: Symbol , peArity :: Int , pePrecedence :: Integer } - deriving Typeable + deriving ( Typeable, Eq ) data ArgumentFilterEntry = ArgumentFilterEntry { afeSymbol :: Symbol , afeArity :: Int , afeFilter :: Either Int [Int] } - deriving Typeable + deriving ( Typeable, Eq ) diff --git a/TPDB/CPF/Proof/Write.hs b/TPDB/CPF/Proof/Write.hs index 3d369fb..b5e8b7c 100644 --- a/TPDB/CPF/Proof/Write.hs +++ b/TPDB/CPF/Proof/Write.hs @@ -86,8 +86,14 @@ instance ( Typeable t, XmlContent t ) instance XmlContent Proof where parseContents = error "parseContents not implemented" - toContents p = case p of - TrsTerminationProof p -> toContents p + toContents p = + let missing t = rmkel t $ rmkel "missing-toContents-instance" [] + in case p of + TrsTerminationProof p -> missing "TrsTerminationProof" + TrsNonterminationProof p -> missing "TrsNonterminationProof" + RelativeTerminationProof p -> missing "RelativeTerminationProof" + RelativeNonterminationProof p -> missing "RelativeNonterminationProof" + ComplexityProof p -> missing "ComplexityProof" instance XmlContent DPS where parseContents = error "parseContents not implemented" diff --git a/tpdb.cabal b/tpdb.cabal index 7d021fe..12f9bc6 100644 --- a/tpdb.cabal +++ b/tpdb.cabal @@ -1,5 +1,5 @@ Name: tpdb -Version: 1.0.0 +Version: 1.0.1 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann Category: Logic