tpdb 1.3.2 → 1.3.3

raw patch · 5 files changed

+108/−36 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• src/TPDB/Data.hs +49/−15
• src/TPDB/Data/Attributes.hs +12/−9
• src/TPDB/XTC/Read.hs +28/−11
• test/read_print_xml_theory.hs +11/−0
• tpdb.cabal +8/−1

@@ -1,3 +1,8 @@+-- | Data types for rewrite systems and termination problems.+-- A "bare" term rewrite system (list of rules and relative rules) is @TRS v s@.+-- A termination problem is @Problem v s@. This contains a rewrite system plus extra+-- information (strategy, theory, etc.)+ {-# language DeriveDataTypeable #-}  module TPDB.Data @@ -20,10 +25,10 @@ import Data.Hashable import Data.Function (on) -data Identifier = +data Identifier =      Identifier { _identifier_hash :: ! Int-                , name :: ! String -                , arity :: Int +                , name :: ! String+                , arity :: Int                 }     deriving ( Eq, Ord, Typeable ) @@ -39,8 +44,26 @@  --------------------------------------------------------------------- +-- | according to XTC spec+data Funcsym = Funcsym+  { fs_name :: String -- ^ should be Text+  , fs_arity :: Int+  , fs_theory :: Maybe Theory+  , fs_replacementmap :: Maybe Replacementmap+  }+  deriving (Show, Typeable) -data RS s r = +data Signature = Signature [ Funcsym ]+               | HigherOrderSignature+  deriving (Show, Typeable)++data Replacementmap = Replacementmap [Int]+  deriving (Show, Typeable)++---------------------------------------------------------------------+++data RS s r =      RS { signature :: [ s ] -- ^ better keep order in signature (?)         , rules :: [ Rule r ]         , separate :: Bool -- ^ if True, write comma between rules@@ -53,36 +76,47 @@ instance Functor (RS s) where     fmap f rs = rs { rules = map (fmap f) $ rules rs } -strict_rules sys = +strict_rules sys =     do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )-weak_rules sys = +weak_rules sys =     do u <- rules sys ; guard $ weak u ; return ( lhs u, rhs u )-equal_rules sys = +equal_rules sys =     do u <- rules sys ; guard $ equal u ; return ( lhs u, rhs u )  type TRS v s = RS s ( Term v s )  type SRS s = RS s [ s ] -data Problem v s = -     Problem { type_ :: Type +data Problem v s =+     Problem { type_ :: Type              , trs :: TRS v s              , strategy :: Maybe Strategy+             , full_signature :: Signature              -- , metainformation :: Metainformation-             , startterm :: Maybe Startterm  +             , startterm :: Maybe Startterm              , attributes :: Attributes              }  data Type = Termination | Complexity-     deriving Show +     deriving Show  data Strategy = Full | Innermost | Outermost      deriving Show -data Startterm = +-- | this is modelled after+-- https://www.lri.fr/~marche/tpdb/format.html+data Theorydecl v s+  = Property Theory [ s ] -- ^ example: "(AC plus)"+  | Equations [ Rule (Term v s) ]+    deriving Typeable++data Theory = A | C | AC+  deriving (Eq, Ord, Read, Show, Typeable)++data Startterm =        Startterm_Constructor_based        | Startterm_Full-     deriving Show     +     deriving Show  ------------------------------------------------------ @@ -95,10 +129,10 @@ mkunary   s = mk 1 s  from_strict_rules :: Bool -> [(t,t)] -> RS i t-from_strict_rules sep rs = +from_strict_rules sep rs =     RS { rules = map ( \ (l,r) ->              Rule { relation = Strict, top = False, lhs = l, rhs = r } ) rs-       , separate = sep +       , separate = sep        }  with_rules sys rs = sys { rules = rs }

@@ -4,7 +4,7 @@  import TPDB.Data.Term import TPDB.Data.Rule-import TPDB.Pretty +import TPDB.Pretty  import qualified Data.Set as S import qualified Data.Map.Strict as M@@ -19,8 +19,9 @@   , right_linear :: Bool   , linear :: Bool   , max_var_count :: Int-  , max_var_depth :: Int+  , max_var_depth :: Int -- ^ value is meaningless if the system has no variables   }+  deriving Show  instance Pretty Attributes where   pretty a = "Attributes" <+> braces ( fsep $ punctuate comma@@ -35,8 +36,8 @@        , "max_var_count =" <+> pretty (max_var_count a)        , "max_var_depth =" <+> pretty (max_var_depth a)        ] )-   + compute_attributes   :: (Ord v, Ord c)   => [Rule (Term v c)] -> Attributes@@ -49,20 +50,23 @@       vcs = map varcount us   in Attributes      { size_of_signature = S.size sig-     , max_arity = maximum $ do+     , max_arity = safe_maximum (-1) $ do        u <- us ; t <- [lhs u, rhs u]        Node f args <- subterms t        return $ length args      , total_term_size = sum term_sizes-     , max_term_size = maximum term_sizes-     , max_term_depth = maximum term_depths+     , max_term_size = safe_maximum (-1) term_sizes+     , max_term_depth = safe_maximum (-1) term_depths      , left_linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ l <= 1      , right_linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ r <= 1      , linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ l == 1 && r == 1 -- FIXME: or (l == r) ?-     , max_var_count = maximum $ map M.size vcs-     , max_var_depth = maximum $ map length $ terms >>= varpos+     , max_var_count = safe_maximum (-1) $ map M.size vcs+     , max_var_depth = safe_maximum (-1) $ map length $ terms >>= varpos      } +safe_maximum x [] = x+safe_maximum x ys = maximum ys+ varcount :: Ord v => Rule (Term v c) -> M.Map v (Int,Int) varcount u = M.mergeWithKey ( \ k l r -> Just (l,r)) ( M.map ( \k -> (k,0))) (M.map ( \k -> (0,k)))         (varcount_term $ lhs u) (varcount_term $ rhs u)@@ -71,4 +75,3 @@ varcount_term t = M.fromListWith (+) $ do   (p, Var v) <- positions t   return (v, 1)-  

@@ -39,7 +39,7 @@     gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub     let c = mk (length gs) nm     returnA -< Node c gs-          + gotoChild tag = proc x -> do     returnA <<< getChildren <<< getChild tag -< x @@ -51,9 +51,11 @@     rs <- getTRS <<< getChild "trs" -< x     st <- getStrategy <<< getChild "strategy" -< x     stt <- listA ( getStartterm <<< getChild "startterm" ) -< x+    sig <- getSignature <<<  getChild "trs" -< x     returnA -< Problem { trs = rs                         , TPDB.Data.strategy = st-                        , type_ = ty +                        , TPDB.Data.full_signature = sig+                        , type_ = ty                         , startterm = case stt of                              [] -> Nothing                              [x] -> x@@ -79,25 +81,40 @@    ) <+> ( proc x -> do returnA -< Nothing )  getTRS = proc x -> do-    sig <- getSignature <<< getChild "signature" -< x+    sig <- getSignature -< x     str <- getRules Strict <<< getChild "rules" -< x     nostr <- listA ( getRules Weak <<< getChild "relrules" <<< getChild "rules" ) -< x     -- FIXME: check that symbols are use with correct arity-    th <- listA ( atTag "theory" ) -< x-    returnA -< case th of-        [] -> RS { signature = sig+    returnA -< RS { signature = case sig of+                       Signature fs -> do f <- fs ; return $ mk (fs_arity f) (fs_name f)+                       HigherOrderSignature {} -> []                   , rules = str ++ concat nostr                   , separate = False -- for TRS, don't need comma between rules                   }-        _  -> error $ unwords [ "cannot handle theories" ] -getSignature = proc x -> do-    returnA <<< listA ( getFuncsym <<< getChild "funcsym" ) -< x+getSignature =+      ( getFOSignature <<< getChild "signature" )+  <+> ( getHOSignature <<< getChild "higherOrderSignature" ) +getFOSignature = proc x -> do+    fs <- listA ( getFuncsym <<< getChild "funcsym" ) -< x+    returnA -< Signature fs++getHOSignature = proc x -> do+    returnA -< HigherOrderSignature+ getFuncsym = proc x -> do     nm <- getText <<< gotoChild "name" -< x-    ar <- getText <<< gotoChild "arity" -< x-    returnA -< mk (read ar) nm+    ar <- getRead <<< gotoChild "arity" -< x+    th <- listA ( getRead <<< gotoChild "theory" ) -< x+    rm <- listA ( listA (getRead <<< gotoChild "entry") <<< gotoChild "replacementmap" ) -< x+    returnA -< Funcsym  { fs_name = nm+                        , fs_arity = ar+                        , fs_theory = case th of [] -> Nothing ; [t] -> Just t+                        , fs_replacementmap = case rm of [] -> Nothing ; [r] -> Just (Replacementmap r)+                        }++getRead = proc x -> do s <- getText -< x ; returnA -< read s  getRules str = proc x -> do     returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x

@@ -0,0 +1,11 @@+import TPDB.Data+import TPDB.Pretty+import TPDB.XTC+import TPDB.Plain.Write++import Control.Monad ( forM, void )++main = void $ do+    [ p ] <- readProblems "test/AC09.xml"+    print $ pretty p+    print $ full_signature p

@@ -1,5 +1,5 @@ Name: tpdb-Version: 1.3.2+Version: 1.3.3 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann Category: Logic@@ -88,3 +88,10 @@   Type: exitcode-stdio-1.0   main-is: attributes.hs   hs-source-dirs: test ++Test-Suite XML-Theory+  Build-Depends: base==4.*, tpdb+  Type: exitcode-stdio-1.0+  main-is: read_print_xml_theory.hs+  hs-source-dirs: test +