tpdb 0.7.1 → 0.8.2

raw patch · 6 files changed

+29/−12 lines, 6 files

Files

• TPDB/CPF/Proof/Type.hs +11/−1
• TPDB/Convert.hs +6/−4
• TPDB/DP.hs +6/−1
• TPDB/Data.hs +2/−2
• TPDB/Xml/Pretty.hs +3/−3
• tpdb.cabal +1/−1

@@ -38,7 +38,7 @@    deriving ( Typeable )        data Proof = TrsTerminationProof TrsTerminationProof-           -- | TrsNonterminationProof  +           --  | TrsNonterminationProof      deriving ( Typeable )  data Sharp i = Sharp i | Plain i@@ -56,9 +56,19 @@                    }        | DpTrans  { dptrans_dps :: DPS                 , markedSymbols :: Bool , dptrans_dpProof :: DpProof }+     | Semlab {  model :: Model +              , trs :: TRS Identifier Identifier+              , trsTerminationProof :: TrsTerminationProof+              }+     | Unlab {  trs :: TRS Identifier Identifier+              , trsTerminationProof :: TrsTerminationProof+              }      | StringReversal { trs :: TRS Identifier Identifier                       , trsTerminationProof :: TrsTerminationProof                         }  +   deriving ( Typeable )++data Model = FiniteModel { carrierSize :: Int }    deriving ( Typeable )         data DpProof = PIsEmpty  

@@ -3,15 +3,17 @@ import TPDB.Data import Control.Monad ( forM, guard ) -srs2trs :: SRS s -> TRS Identifier s+srs2trs :: SRS Identifier -> TRS Identifier Identifier srs2trs s = s { separate = False               , rules = map convert_srs_rule $ rules s               }    convert_srs_rule u = -    let v = mk 0 "x" -    in  u { lhs = unspine v $ lhs u-          , rhs = unspine v $ rhs u        +    let v = mk 0 "x"+        set_arity a s = s { arity = a }+        handle = unspine v . map (set_arity 1)+    in  u { lhs = handle $ lhs u+          , rhs = handle $ rhs u                   }                     trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )

@@ -33,6 +33,7 @@        os = map ( \ u -> Rule { relation = Weak                                , lhs = fmap Original $ lhs u                                  , rhs = fmap Original $ rhs u  +                               , top = False                                } )            $ rules s        defined = S.fromList $ do @@ -43,5 +44,9 @@             u <- rules s             (_, r @ (Node f args)) <- positions $ rhs u             guard $ S.member f defined-            return $ u { lhs = marked $ lhs u, rhs = marked r }+            return $ Rule { relation = Strict+                          , lhs = marked $ lhs u+                          , rhs = marked r +                          , top = True+                          }    in RS { rules = us ++ os, separate = separate s } 

@@ -94,8 +94,8 @@ type TES = TRS Identifier Identifier type SES = SRS Identifier -mknullary s = Identifier { arity = 0, name = s }-mkunary s = Identifier { arity = 1, name = s }+mknullary s = mk 0 s+mkunary   s = mk 1 s  from_strict_rules :: Bool -> [(t,t)] -> RS i t from_strict_rules sep rs = 

@@ -1,11 +1,11 @@ -- | original author: Malcolm Wallace,  -- license: LGPL -- http://hackage.haskell.org/packages/archive/HaXml/1.23.3/doc/html/Text-XML-HaXml-Pretty.html-+-- -- modified by Johannes Waldmann -- to use a different pretty-printer back-end.---- | This is a pretty-printer for turning the internal representation+--+-- This is a pretty-printer for turning the internal representation --   of generic structured XML documents into the Doc type (which can --   later be rendered using Text.PrettyPrint.HughesPJ.render). --   Essentially there is one pp function for each type in

@@ -1,5 +1,5 @@ Name: tpdb-Version: 0.7.1+Version: 0.8.2 Author: Johannes Waldmann Maintainer: Johannes Waldmann Category: Science