tpdb 2.1.1 → 2.2.0

raw patch · 6 files changed

+70/−12 lines, 6 filesnew-component:exe:srs2trs

Files

• src/TPDB/Data.hs +30/−1
• src/TPDB/Data/Term.hs +1/−0
• src/TPDB/Plain/Write.hs +11/−6
• src/TPDB/XTC/Read.hs +7/−4
• srs2trs.hs +15/−0
• tpdb.cabal +6/−1

@@ -3,7 +3,10 @@ -- A termination problem is @Problem v s@. This contains a rewrite system plus extra -- information (strategy, theory, etc.) -{-# language DeriveDataTypeable #-}+{-# language DeriveDataTypeable,+    FlexibleInstances, FlexibleContexts,+    MultiParamTypeClasses, TypeFamilies+#-}  module TPDB.Data  @@ -22,9 +25,11 @@ import Data.Typeable import Control.Monad ( guard ) +import Data.Void import Data.Hashable import Data.Function (on) import qualified Data.Text as T+import qualified Data.Set as S  data Identifier =      Identifier { _identifier_hash :: ! Int@@ -42,7 +47,18 @@ mk a n = Identifier { _identifier_hash = hash (a,n)                     , arity = a, name = n } +class Ord (Var t) => Variables t where+  type Var t+  variables :: t -> S.Set (Var t) +instance Ord v => Variables (Term v c) where+  type Var (Term v c) = v+  variables = vars++instance Variables [c] where+  type Var [c] = ()+  variables _ = S.empty+ ---------------------------------------------------------------------  -- | according to XTC spec@@ -87,6 +103,19 @@ type TRS v s = RS s ( Term v s )  type SRS s = RS s [ s ]++instance Variables r => Variables (Rule r) where+  type Var (Rule r) = Var r+  variables u =+    S.unions [ variables (lhs u), variables (rhs u) ]++instance Ord v => Variables (TRS v s) where+  type Var (TRS v s) = v+  variables sys = S.unions $ map variables $ rules sys++instance Variables (SRS s) where+  type Var (SRS s) = Void+  variables sys = S.empty  data Problem v s =      Problem { type_ :: Type

@@ -177,3 +177,4 @@ -- | list of variables (in pre-order, with duplicates) voccs :: Term v c -> [ v ] voccs t = do ( p, Var v ) <- positions t ; return v+

@@ -3,6 +3,7 @@  {-# language FlexibleContexts #-} {-# language OverloadedStrings #-}+{-# language UndecidableInstances #-}  module TPDB.Plain.Write where @@ -11,6 +12,7 @@  import Data.List ( nub ) import Data.String ( fromString )+import qualified Data.Set as S import qualified Data.Text as T  instance Pretty Identifier where@@ -42,19 +44,22 @@ instance ( Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where     prettyTerm = pretty -instance ( Pretty s, PrettyTerm r ) => Pretty ( RS s r ) where+instance ( Pretty s, PrettyTerm r, Variables (RS s r)+  , Pretty (Var (RS s r)))+  => Pretty ( RS s r ) where     pretty sys = vcat -        [ parens $ "RULES" <+>+        [ let vs = S.toList $ variables sys+	  in if null vs+	     then empty   +	     else parens $ "VAR" <+> vcat (map pretty vs)+	, parens $ "RULES" <+>           vcat ( ( if separate sys then punctuate comma else id )                  $ map pretty $ rules sys                 )-        -- FIXME: variables are not shown (and it is impossible to compute-        -- them here, this is actually a TPDB format design error, -        -- since variables should be local (per rule), not global)         -- FIXME: output strategy, theory         ] -instance ( Pretty s, Pretty r ) => Pretty ( Problem s r ) where+instance ( Pretty s, Pretty r, Variables (Term s r) ) => Pretty ( Problem s r ) where     pretty p = vcat        [ pretty $ trs p         , case strategy p of  

@@ -1,6 +1,8 @@ -- | construct data object from XML tree. -{-# language NoMonomorphismRestriction, PatternSignatures, OverloadedStrings #-}+{-# language NoMonomorphismRestriction, PatternSignatures, OverloadedStrings+  , BangPatterns+#-}   module TPDB.XTC.Read (readProblemF, readProblemT ) where@@ -26,11 +28,12 @@     ps -> error "input contains more than one XTC problem"  readProblemT :: LT.Text -> Either SomeException (Problem Identifier Identifier)-readProblemT t = do-  [p] <- ( getProblem . fromDocument ) <$> Text.XML.parseText Text.XML.def t-  return p+readProblemT t = case ( getProblem . fromDocument ) <$> Text.XML.parseText Text.XML.def t of+  Right [ p ] -> Right p+  Left ex -> Left ex  +getProblem :: Cursor -> [ Problem Identifier Identifier ] getProblem = element "problem" >=> \ c -> do     let ! ty = case c $| attribute "type" of          [ "termination" ] -> Termination

@@ -0,0 +1,15 @@+{-# language LambdaCase #-}++module Main where++import TPDB.Input (get_srs)+import TPDB.Pretty+import TPDB.Plain.Write+import TPDB.Convert (srs2trs)+import System.IO (stdout)+import System.Environment++main = getArgs >>= \ case+  [ fp ] -> displayIO stdout . renderWide . pretty . srs2trs =<< get_srs fp+  +  

@@ -1,5 +1,6 @@ Name: tpdb-Version: 2.1.1+Version: 2.2.0+ Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann Category: Logic@@ -47,6 +48,10 @@ Executable plain2xtc   build-depends: base==4.*, tpdb, bytestring   main-is: plain2xtc.hs++Executable srs2trs+  build-depends: base==4.*, tpdb, bytestring+  main-is: srs2trs.hs  -- Executable Compressor --     Main-is: Compressor.hs