tpdb 0.9.6 → 0.9.8

raw patch · 4 files changed

+71/−16 lines, 4 files

Files

• TPDB/CPF/Proof/Read.hs +42/−14
• TPDB/CPF/Proof/Type.hs +24/−0
• TPDB/CPF/Proof/Write.hs +4/−1
• tpdb.cabal +1/−1

@@ -15,6 +15,9 @@ import Control.Arrow.ArrowList import Control.Arrow.ArrowTree +import qualified TPDB.CPF.Proof.Write as W -- for testing+import qualified Text.XML.HXT.Arrow.XmlState as X + {- | dangerous:  not all constructor arguments will be set. the function produces something like@@ -25,33 +28,58 @@ -}  readCP :: String -> IO [ CertificationProblem ]-readCP s = runX ( readString [] s >>> getCP )+readCP s = runX ( X.withTraceLevel 0 $ readString [] s >>> getCP )  getCP = atTag "certificationProblem" >>> proc x -> do     inp <- getInput <<< getChild "input" -< x     pro <- getProof <<< getChild "proof" -< x-    returnA -< CertificationProblem { input = inp, proof = pro }+    ver <- getText <<< gotoChild "cpfVersion" -< x+    returnA -< CertificationProblem { input = inp, proof = pro, cpfVersion = "2.2" } -getInput = atTag "input" >>> proc x -> do-    trsI <- getTrsInput <<< getChild "trsInput" -< x+getInput = getTerminationInput <+> getComplexityInput++getTerminationInput = atTag "input" >>> proc x -> do+    trsI <- getTrsInput <<< getChild "trsInput" -< x         returnA -< TrsInput $ RS { rules = trsI, separate = False } +getComplexityInput = atTag "input" >>> proc x -> do+    y <- getChild "complexityInput" -< x+    trsI <- getTrsInput <<< getChild "trsInput" -< y+    cm <- getComplexityMeasure -< y+    cc <- getComplexityClass -< y+    returnA -< ComplexityInput+        { trsinput_trs = RS { rules = trsI, separate = False }+        , complexityMeasure = cm+        , complexityClass = cc+        }++getComplexityMeasure = +        getDummy "derivationalComplexity" DerivationalComplexity+    <+> getDummy "runtimeComplexity" RuntimeComplexity++getComplexityClass = proc x -> do+    d <- getText <<< gotoChild "polynomial" -< x+    returnA -< ComplexityClassPolynomial { degree = read d }+ getTrsInput = proc x -> do     sys <- getTrs <<< getChild "trs" -< x-    returnA -< sys--getTrs = proc x -> do-    str <- getRules Strict <<< getChild "rules" -< x-    returnA -< str+    rels <- listA ( getTrsWith Weak <<< getChild "relativeRules" ) -< x+    returnA -< sys ++ concat rels -getProof = getTrsTerminationProof <+> getTrsNonterminationProof+getTrs = getTrsWith Strict -getTrsTerminationProof = atTag "trsTerminationProof" >>> proc x -> do-    returnA -< TrsTerminationProof undefined+getTrsWith s = proc x -> do+    str <- getRules s <<< getChild "rules" -< x+    returnA -< str -getTrsNonterminationProof = atTag "trsNonterminationProof" >>> proc x -> do-    returnA -< TrsNonterminationProof undefined+getProof = getDummy "trsTerminationProof" ( TrsTerminationProof undefined )+       <+> getDummy "trsNonTerminationProof" ( TrsNonterminationProof undefined )+       <+> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined )+       <+> getDummy "relativeNonTerminationProof" ( RelativeNonterminationProof undefined )+       <+> getDummy "complexityProof" ( ComplexityProof undefined ) +getDummy t c = atTag t >>> proc x -> do+    returnA -< c   getRules str = proc x -> do     returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x

@@ -35,15 +35,39 @@       -- ^ 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)+    | ComplexityInput { trsinput_trs :: TRS Identifier Identifier+                      , complexityMeasure :: ComplexityMeasure+                      , complexityClass :: ComplexityClass      +                      }    deriving ( Typeable )        data Proof = TrsTerminationProof TrsTerminationProof            | TrsNonterminationProof TrsNonterminationProof+           | RelativeTerminationProof TrsTerminationProof+           | RelativeNonterminationProof TrsNonterminationProof+           | ComplexityProof ComplexityProof    deriving ( Typeable )  data DPS = forall s . ( XmlContent s , Typeable s )          => DPS [ Rule (Term Identifier s) ]    deriving ( Typeable )++++data ComplexityProof = ComplexityProofFIXME ()+    deriving ( Typeable )++data ComplexityMeasure +     = DerivationalComplexity+     | RuntimeComplexity+    deriving ( Typeable )++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 )  data TrsNonterminationProof = TrsNonterminationProofFIXME ()     deriving ( Typeable )

@@ -63,6 +63,9 @@     toContents i = case i of       TrsInput {} -> rmkel "trsInput" $ toContents ( symbolize $ trsinput_trs i )+      ComplexityInput {} -> rmkel "complexityInput" $ concat+          [ rmkel "trsInput" $ toContents $ symbolize $ trsinput_trs i+          ]  instance XmlContent ( T.TRS Identifier Symbol ) where    parseContents = error "parseContents not implemented"@@ -164,7 +167,7 @@     toContents dgc = rmkel "component" $ concat $         [ {- rmkel "dps" $ -} toContents $ dgcDps dgc         , rmkel "realScc" -           -- $ toContents $ dgcRealScc dgc+           --  $ toContents $ dgcRealScc dgc            -- NO, Bool is encoded as text, not as attribute             [ nospaceString $ map toLower $ show $ dgcRealScc dgc ]         ] ++ 

@@ -1,5 +1,5 @@ Name: tpdb-Version: 0.9.6+Version: 0.9.8 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann Category: Logic