tpdb 2.8.0 → 2.8.1

raw patch · 3 files changed

+24/−8 lines, 3 files

Files

• src/TPDB/CPF/Proof/Type.hs +10/−2
• src/TPDB/CPF/Proof/Write.hs +12/−4
• tpdb.cabal +2/−2

@@ -35,15 +35,23 @@ cp = CertificationProblem   { cpfVersion = "3.4"   , input = TrsInput-    { trsinput_trs = RS { rules = [ ru ] }+    { trsinput_trs = RS { rules = [ rs, rw ] }     }   , proof = TrsTerminationProof RIsEmpty   , origin = ignoredOrigin   } -ru = let a = SymName $ mk 0 "s" in Rule+rs = let a = SymName $ mk 0 "s" in Rule         { top = False         , relation = TPDB.Data.Strict+        , lhs = Node a []+        , rhs = Node a []+        , original_variable = Nothing+        }++rw = let a = SymName $ mk 0 "s" in Rule+        { top = False+        , relation = TPDB.Data.Weak         , lhs = Node a []         , rhs = Node a []         , original_variable = Nothing

@@ -66,7 +66,16 @@    parseContents = error "parseContents not implemented"     toContents i = case i of-      TrsInput {} -> rmkel "trsInput" $ toContents (trsinput_trs i )+      TrsInput {} ->+        let sys = trsinput_trs i+            s = standard sys+            r = relative sys+        in  rmkel "trsInput" $+                toContents s+                <> if null (T.rules r) then []+                   else rmkel "relativeRules" $+                        rmkel "rules" $+                        concatMap toContents $ T.rules r       ComplexityInput {} -> rmkel "complexityInput" $ concat           [ rmkel "trsInput" $ toContents $ trsinput_trs i           ]@@ -153,7 +162,7 @@ instance XmlContent (TrsTerminationProof Relative) where    parseContents = error "parseContents not implemented" -   toContents p = rmkel "relativeTerminationProof" $ case p of+   toContents p = rmkel "trsTerminationProof" $ case p of       RIsEmpty -> rmkel "rIsEmpty" []       SIsEmpty {} -> rmkel "sIsEmpty" $ concat           [ toContents $ trsTerminationProof_Standard p@@ -178,8 +187,7 @@           ]       RuleRemoval {} -> rmkel "ruleRemoval" $ concat           [ toContents $ rr_orderingConstraintProof p-          , toContents $ standard $ trs p-          , toContents $ relative $ trs p+          , toContents $ trs_deleted p           , toContents $ trsTerminationProof p           ]       EqualityRemoval {} -> rmkel "equalityRemoval" $ concat

@@ -1,7 +1,7 @@-Cabal-Version: 3.0+Cabal-Version: 3.8  Name: tpdb-Version: 2.8.0+Version: 2.8.1  Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann