tpdb 0.9.8 → 1.1.1

raw patch · 7 files changed

+92/−50 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• TPDB/CPF/Proof/Read.hs +13/−9
• TPDB/CPF/Proof/Type.hs +43/−33
• TPDB/CPF/Proof/Write.hs +10/−3
• TPDB/DP/Unify.hs +20/−1
• TPDB/Data.hs +4/−2
• TPDB/Xml.hs +1/−1
• tpdb.cabal +1/−1

@@ -28,21 +28,24 @@ -}  readCP :: String -> IO [ CertificationProblem ]-readCP s = runX ( X.withTraceLevel 0 $ readString [] s >>> getCP )+readCP = readCP_with_tracelevel 0 -getCP = atTag "certificationProblem" >>> proc x -> do+readCP_with_tracelevel l s = runX ( X.withTraceLevel l $ readString [] s >>> getCP )++getCP = getChild "certificationProblem" >>> proc x -> do     inp <- getInput <<< getChild "input" -< x     pro <- getProof <<< getChild "proof" -< x     ver <- getText <<< gotoChild "cpfVersion" -< x-    returnA -< CertificationProblem { input = inp, proof = pro, cpfVersion = "2.2" }+    returnA -< CertificationProblem +        { input = inp, proof = pro, cpfVersion = ver, origin = ignoredOrigin }  getInput = getTerminationInput <+> getComplexityInput -getTerminationInput = atTag "input" >>> proc x -> do+getTerminationInput = hasName "input" >>> proc x -> do     trsI <- getTrsInput <<< getChild "trsInput" -< x         returnA -< TrsInput $ RS { rules = trsI, separate = False } -getComplexityInput = atTag "input" >>> proc x -> do+getComplexityInput = hasName "input" >>> proc x -> do     y <- getChild "complexityInput" -< x     trsI <- getTrsInput <<< getChild "trsInput" -< y     cm <- getComplexityMeasure -< y@@ -73,12 +76,13 @@     returnA -< str  getProof = getDummy "trsTerminationProof" ( TrsTerminationProof undefined )-       <+> getDummy "trsNonTerminationProof" ( TrsNonterminationProof undefined )+       <+> getDummy "trsNonterminationProof" ( TrsNonterminationProof undefined )        <+> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined )-       <+> getDummy "relativeNonTerminationProof" ( RelativeNonterminationProof undefined )+       <+> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined )        <+> getDummy "complexityProof" ( ComplexityProof undefined ) -getDummy t c = atTag t >>> proc x -> do+getDummy t c = proc x -> do +    getChild t -< x     returnA -< c   getRules str = proc x -> do@@ -109,5 +113,5 @@ getChild tag = proc x -> do     returnA <<< hasName tag <<< isElem <<< getChildren -< x -atTag tag = deep (isElem >>> hasName tag)+ 

@@ -1,4 +1,6 @@-{-# OPTIONS -fglasgow-exts #-}+{-# language StandaloneDeriving #-}+{-# language ExistentialQuantification #-}+{-# language DeriveDataTypeable #-}  -- | internal representation of CPF termination proofs, -- see <http://cl-informatik.uibk.ac.at/software/cpf/>@@ -23,13 +25,18 @@                           , proof :: Proof                            , origin :: Origin                             }  -   deriving ( Typeable )+   deriving ( Typeable, Eq ) -data Origin = ProofOrigin Tool -    deriving Typeable-data Tool = Tool { name :: String , version :: String } -    deriving Typeable+data Origin = ProofOrigin { tool :: Tool }+    deriving ( Typeable, Eq ) +ignoredOrigin = ProofOrigin { tool = Tool "ignored" "ignored"  }++data Tool = Tool { name :: String +                 , version :: String+                 } +    deriving ( Typeable, Eq )+ data CertificationProblemInput      = TrsInput { trsinput_trs :: TRS Identifier Identifier }       -- ^ this is actually not true, since instead of copying from XTC,@@ -39,38 +46,39 @@                       , complexityMeasure :: ComplexityMeasure                       , complexityClass :: ComplexityClass                             }-   deriving ( Typeable )      +   deriving ( Typeable, Eq )        data Proof = TrsTerminationProof TrsTerminationProof            | TrsNonterminationProof TrsNonterminationProof            | RelativeTerminationProof TrsTerminationProof            | RelativeNonterminationProof TrsNonterminationProof            | ComplexityProof ComplexityProof-   deriving ( Typeable )+   deriving ( Typeable, Eq ) -data DPS = forall s . ( XmlContent s , Typeable s ) +data DPS = forall s . ( XmlContent s , Typeable s, Eq s )          => DPS [ Rule (Term Identifier s) ]    deriving ( Typeable ) +instance Eq DPS where x == y = error "instance Eq DPS"   data ComplexityProof = ComplexityProofFIXME ()-    deriving ( Typeable )+    deriving ( Typeable, Eq )  data ComplexityMeasure       = DerivationalComplexity      | RuntimeComplexity-    deriving ( Typeable )+    deriving ( Typeable, Eq )  data ComplexityClass =       ComplexityClassPolynomial { degree :: Int }       -- ^ it seems the degree must always be given in CPF,      -- although the category spec also allows "POLY"      -- http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php-    deriving ( Eq, Typeable )+    deriving ( Typeable, Eq )  data TrsNonterminationProof = TrsNonterminationProofFIXME ()-    deriving ( Typeable )+    deriving ( Typeable, Eq )  data TrsTerminationProof       = RIsEmpty@@ -90,10 +98,10 @@      | StringReversal { trs :: TRS Identifier Identifier                       , trsTerminationProof :: TrsTerminationProof                         }  -   deriving ( Typeable )+   deriving ( Typeable, Eq )  data Model = FiniteModel Int [Interpret]-   deriving ( Typeable )+   deriving ( Typeable, Eq )         data DpProof = PIsEmpty                | RedPairProc { rppOrderingConstraintProof :: OrderingConstraintProof@@ -112,53 +120,53 @@                           , ulpTrs :: DPS                           , ulpDpProof :: DpProof                           }-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data DepGraphComponent =      DepGraphComponent { dgcRealScc :: Bool                        , dgcDps :: DPS                        , dgcDpProof :: DpProof                        }-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data OrderingConstraintProof = OCPRedPair RedPair-                             deriving ( Typeable )+                             deriving ( Typeable, Eq )  data RedPair = RPInterpretation Interpretation              | RPPathOrder      PathOrder-             deriving ( Typeable )+             deriving ( Typeable, Eq )  data Interpretation =      Interpretation { interpretation_type :: Interpretation_Type                     , interprets :: [ Interpret  ]                     }-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data Interpretation_Type =     Matrix_Interpretation { domain :: Domain, dimension :: Int                          , strictDimension :: Int                          }-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data Domain = Naturals              | Rationals Rational             | Arctic Domain             | Tropical Domain-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data Interpret = Interpret      { symbol :: Symbol , arity :: Int , value :: Value }-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data Value = Polynomial    Polynomial            | ArithFunction ArithFunction-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data Polynomial = Sum [ Polynomial ]                 | Product [ Polynomial ]                 | Polynomial_Coefficient Coefficient                 | Polynomial_Variable String-   deriving ( Typeable )+   deriving ( Typeable, Eq )  data ArithFunction = AFNatural  Integer                    | AFVariable Integer@@ -167,39 +175,41 @@                    | AFMin      [ArithFunction]                    | AFMax      [ArithFunction]                    | AFIfEqual  ArithFunction ArithFunction ArithFunction ArithFunction-                   deriving ( Typeable )+                   deriving ( Typeable, Eq )  data Symbol = SymName  Identifier             | SymSharp Symbol             | SymLabel Symbol Label-            deriving ( Typeable )+            deriving ( Typeable, Eq )  data Label = LblNumber [Integer]            | LblSymbol [Symbol]-           deriving ( Typeable )+           deriving ( Typeable, Eq )  data Coefficient = Vector [ Coefficient ]            | Matrix [ Coefficient ]-           | forall a . XmlContent a => Coefficient_Coefficient a+           | forall a . (Eq a, XmlContent a ) => Coefficient_Coefficient a    deriving ( Typeable ) +instance Eq Coefficient where x == y = error "instance Eq Coefficient"+ data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite-   deriving Typeable+   deriving ( Typeable, Eq )  class ToExotic a where toExotic :: a -> Exotic  data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]-               deriving Typeable+               deriving ( Typeable, Eq )  data PrecedenceEntry = PrecedenceEntry { peSymbol     :: Symbol                                        , peArity      :: Int                                        , pePrecedence :: Integer                                        }-                     deriving Typeable+                     deriving ( Typeable, Eq )  data ArgumentFilterEntry =       ArgumentFilterEntry { afeSymbol :: Symbol                          , afeArity  :: Int                          , afeFilter :: Either Int [Int]                          }-     deriving Typeable+     deriving ( Typeable, Eq )

@@ -12,7 +12,7 @@  import Text.XML.HaXml.Types (QName (..) ) import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )-import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..) )+import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..), Misc (PI) )  import TPDB.Xml  import TPDB.Data.Xml @@ -30,7 +30,8 @@ tox :: CertificationProblem -> Document () tox p =      let xd = XMLDecl "1.0" ( Just $ EncodingDecl "UTF-8" ) Nothing -        pro = Prolog ( Just xd ) [] Nothing []+        style = PI ("xml-stylesheet", "type=\"text/xsl\" href=\"cpfHTML.xsl\"")+        pro = Prolog ( Just xd ) [] Nothing [style]         [ CElem e _ ] = toContents p     in  Document pro emptyST e [] @@ -85,8 +86,14 @@ instance XmlContent Proof where    parseContents = error "parseContents not implemented" -   toContents p = case p of+   toContents p = +     let missing t = rmkel t $ rmkel "missing-toContents-instance" [] +     in  case p of        TrsTerminationProof p -> toContents p+       TrsNonterminationProof p -> missing "TrsNonterminationProof"+       RelativeTerminationProof p -> missing "RelativeTerminationProof"+       RelativeNonterminationProof p -> missing "RelativeNonterminationProof"+       ComplexityProof p -> missing "ComplexityProof"  instance XmlContent DPS where    parseContents = error "parseContents not implemented"

@@ -1,4 +1,4 @@-module TPDB.DP.Unify ( mgu, unifies, apply, times ) where+module TPDB.DP.Unify ( mgu, match, unifies, apply, times ) where  import TPDB.Data import qualified Data.Map as M@@ -8,6 +8,25 @@ type Substitution v c = M.Map v (Term v c)  unifies t1 t2 = isJust $ mgu t1 t2++-- | view variables as symbols+pack :: Term v c -> Term any (Either v c)+pack ( Var v ) = Node ( Left v ) []+pack ( Node f args ) = Node ( Right f ) ( map pack args )++unpack :: Term any (Either v c) -> Term v c+unpack ( Node ( Left v ) [] ) = Var v+unpack ( Node ( Right f ) args ) = Node f ( map unpack args )++-- | will only bind variables in the left side+match :: ( Ord v, Ord w, Eq c )+      => Term v c+      -> Term w c+      -> Maybe ( M.Map v ( Term w c ) )+match l r = do+    u <- mgu ( fmap Right l ) ( pack r )+    return $ M.map unpack  u+  -- | naive implementation (worst case exponential) mgu

@@ -18,8 +18,10 @@ import Data.Function (on)  data Identifier = -     Identifier { _identifier_hash :: Int-                , name :: String , arity :: Int }+     Identifier { _identifier_hash :: ! Int+                , name :: ! String +                , arity :: Int +                }     deriving ( Eq, Ord, Typeable )  instance Hashable Identifier where

@@ -14,7 +14,7 @@ rmkel name cs = return $ mkel name cs  nospaceString :: String -> Content ()-nospaceString s = CString False s ()+nospaceString s = CString False (escape s) ()  instance Typeable t => HTypeable t where      toHType x = let cs = show ( typeOf x ) in Prim cs cs

@@ -1,5 +1,5 @@ Name: tpdb-Version: 0.9.8+Version: 1.1.1 Author: Alexander Bau, Johannes Waldmann Maintainer: Johannes Waldmann Category: Logic