tpdb 2.8.3 → 2.8.4

raw patch · 5 files changed

+36/−11 lines, 5 files

Files

• src/TPDB/CPF/Proof/Read.hs +8/−2
• src/TPDB/CPF/Proof/Type.hs +11/−4
• src/TPDB/CPF/Proof/Write.hs +15/−3
• src/TPDB/Data.hs +1/−1
• tpdb.cabal +1/−1

@@ -3,7 +3,7 @@ module TPDB.CPF.Proof.Read where  import TPDB.CPF.Proof.Type as Type-import TPDB.Data+import TPDB.Data hiding (Type (..))  {- import Text.XML.HXT.Arrow.XmlArrow@@ -65,10 +65,17 @@   ( CertificationProblem      <$> (c $/ element "cpfVersion" &/ content )      <*> (c $/ element "input" &/ getInput )+     <*> (c $/ element "property" &/ getProperty )+     <*> (c $/ element "answer" &/ getAnswer )      <*> (c $/ element "proof" &/ getProof)      <*> (c $/ element "origin" >=> return [ignoredOrigin] )   ) +getProperty = (element "termination" >> return [ Termination])++getAnswer = (element "no" >> return [No])+       <>   (element "yes" >> return [Yes])+ getInput =  getTerminationInput    <> getComplexityInput    <> getACTerminationInput@@ -85,7 +92,6 @@       , asymbols = as       , csymbols = cs       }-  getComplexityInput = element "input" >=> \ c -> do     trsI <- c $/ element "complexityInput" &/ element "trsInput" &/ getTrsInput

@@ -18,7 +18,7 @@  where -import TPDB.Data+import TPDB.Data hiding (Type(..)) import TPDB.Plain.Write () import Data.Typeable import TPDB.Pretty@@ -33,10 +33,12 @@  cp :: CertificationProblem cp = CertificationProblem-  { cpfVersion = "3.4"+  { cpfVersion = "3.6"   , input = TrsInput     { trsinput_trs = RS { rules = [ rs, rw ] }     }+  , property = Termination+  , answer = Yes   , proof = TrsTerminationProof RIsEmpty   , origin = ignoredOrigin   }@@ -57,10 +59,15 @@         , original_variable = Nothing         } +data Property = Termination deriving (Typeable, Eq, Generic)+data Answer = No | Yes deriving (Typeable, Eq, Generic)+ data CertificationProblem =      CertificationProblem { cpfVersion :: Text-                          , input :: CertificationProblemInput-                          , proof :: Proof +                          , input :: !CertificationProblemInput+                          , property :: !Property+                          , answer :: !Answer+                          , proof :: !Proof                            , origin :: Origin                             }      deriving ( Typeable, Eq, Generic )

@@ -42,12 +42,21 @@          [ mkel "cpfVersion" [ nospaceString $ cpfVersion cp ]          , mkel "lookupTables"  []          , mkel "input" $ toContents ( input cp )-         , mkel "property" $ rmkel "termination" []-         , mkel "answer" $ rmkel "yes" [] -- FIXME (no?)+         , mkel "property" $ toContents (property cp)+         , mkel "answer" $ toContents (answer cp)          , mkel "proof" $ toContents ( proof cp )          , mkel "origin" $ toContents ( origin cp )          ] +instance XmlContent Property where+  toContents p = case p of+    Termination -> rmkel "termination" []++instance XmlContent Answer where+  toContents a = case a of+    No -> rmkel "no" []+    Yes -> rmkel "yes" []+ instance XmlContent Origin where    parseContents = error "parseContents not implemented" @@ -168,7 +177,8 @@           [ toContents $ trsTerminationProof_Standard p           ]       StringReversal {} -> rmkel "stringReversal" $ concat-          [ toContents $ standard $ trs p+          [ -- toContents $ trs p+            toContents $ standard $ trs p           , toContents $ relative $ trs p           , toContents $ trsTerminationProof p           ]@@ -198,6 +208,8 @@  standard trs = trs `T.with_rules` filter T.strict (T.rules trs) relative trs = trs `T.with_rules` filter T.weak   (T.rules trs)++toco_relative s = [ toContents s ]  toco_relative s =        [ toContents $ standard s ]

@@ -115,7 +115,7 @@              }  data Type = Termination | Complexity-     deriving Show+  deriving Show  data Strategy = Full | Innermost | Outermost      deriving Show

@@ -1,7 +1,7 @@ Cabal-Version: 3.8  Name: tpdb-Version: 2.8.3+Version: 2.8.4  Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann