diff --git a/TPDB/CPF/Proof/Read.hs b/TPDB/CPF/Proof/Read.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/CPF/Proof/Read.hs
@@ -0,0 +1,85 @@
+{-# language Arrows, NoMonomorphismRestriction, PatternSignatures #-}
+
+module TPDB.CPF.Proof.Read where
+
+import TPDB.CPF.Proof.Type
+import TPDB.Data
+
+import Text.XML.HXT.Arrow.XmlArrow
+
+import Text.XML.HXT.Arrow.XmlState ( runX )
+import Text.XML.HXT.Arrow.ReadDocument ( readString )
+import Text.XML.HXT.Arrow.XmlOptions ( a_validate )
+import Text.XML.HXT.DOM.XmlKeywords (v_0)
+import Control.Arrow
+import Control.Arrow.ArrowList
+import Control.Arrow.ArrowTree
+
+{- | dangerous:
+not all constructor arguments will be set.
+the function produces something like
+
+ CertificationProblem { input = CertificationProblemInput
+ , proof = TrsTerminationProof undefined
+ }
+-}
+
+readCP :: String -> IO [ CertificationProblem ]
+readCP s = runX ( readString [] s >>> getCP )
+
+getCP = atTag "certificationProblem" >>> proc x -> do
+ inp <- getInput <<< getChild "input" -< x
+ pro <- getProof <<< getChild "proof" -< x
+ returnA -< CertificationProblem { input = inp, proof = pro }
+
+getInput = atTag "input" >>> proc x -> do
+ trsI <- getTrsInput <<< getChild "trsInput" -< x
+ returnA -< TrsInput $ RS { rules = trsI, separate = False }
+
+getTrsInput = proc x -> do
+ sys <- getTrs <<< getChild "trs" -< x
+ returnA -< sys
+
+getTrs = proc x -> do
+ str <- getRules Strict <<< getChild "rules" -< x
+ returnA -< str
+
+getProof = getTrsTerminationProof <+> getTrsNonterminationProof
+
+getTrsTerminationProof = atTag "trsTerminationProof" >>> proc x -> do
+ returnA -< TrsTerminationProof undefined
+
+getTrsNonterminationProof = atTag "trsNonterminationProof" >>> proc x -> do
+ returnA -< TrsNonterminationProof undefined
+
+
+getRules str = proc x -> do
+ returnA <<< listA ( getRule str <<< getChild "rule" ) -< x
+
+getRule str = proc x -> do
+ l <- getTerm <<< isElem <<< gotoChild "lhs" -< x
+ r <- getTerm <<< isElem <<< gotoChild "rhs" -< x
+ returnA -< Rule { lhs = l, relation = str, rhs = r, top = False }
+
+
+getTerm = getVar <+> getFunApp
+
+getVar = proc x -> do
+ nm <- getText <<< getChildren <<< hasName "var" -< x
+ returnA -< Var $ mk 0 nm
+
+getFunApp = proc x -> do
+ sub <- hasName "funapp" -< x
+ nm <- getText <<< gotoChild "name" -< sub
+ 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
+
+getChild tag = proc x -> do
+ returnA <<< hasName tag <<< isElem <<< getChildren -< x
+
+atTag tag = deep (isElem >>> hasName tag)
+
diff --git a/TPDB/CPF/Proof/Type.hs b/TPDB/CPF/Proof/Type.hs
--- a/TPDB/CPF/Proof/Type.hs
+++ b/TPDB/CPF/Proof/Type.hs
@@ -38,16 +38,16 @@
deriving ( Typeable )
data Proof = TrsTerminationProof TrsTerminationProof
- -- | TrsNonterminationProof
+ | TrsNonterminationProof TrsNonterminationProof
deriving ( Typeable )
-data Sharp i = Sharp i | Plain i
- deriving ( Typeable, Eq, Ord )
-
data DPS = forall s . ( XmlContent s , Typeable s )
=> DPS [ Rule (Term Identifier s) ]
deriving ( Typeable )
+data TrsNonterminationProof = TrsNonterminationProofFIXME ()
+ deriving ( Typeable )
+
data TrsTerminationProof
= RIsEmpty
| RuleRemoval { rr_orderingConstraintProof :: OrderingConstraintProof
@@ -68,18 +68,42 @@
}
deriving ( Typeable )
-data Model = FiniteModel { carrierSize :: Int }
+data Model = FiniteModel Int [Interpret]
deriving ( Typeable )
data DpProof = PIsEmpty
- | RedPairProc { dp_orderingConstraintProof :: OrderingConstraintProof
- , red_pair_dps :: DPS , redpairproc_dpProof :: DpProof }
+ | RedPairProc { rppOrderingConstraintProof :: OrderingConstraintProof
+ , rppDps :: DPS
+ , rppUsableRules :: Maybe DPS
+ , rppDpProof :: DpProof
+ }
+ | DepGraphProc [ DepGraphComponent ]
+
+ | SemLabProc { slpModel :: Model
+ , slpDps :: DPS
+ , slpTrs :: DPS
+ , slpDpProof :: DpProof
+ }
+ | UnlabProc { ulpDps :: DPS
+ , ulpTrs :: DPS
+ , ulpDpProof :: DpProof
+ }
deriving ( Typeable )
-data OrderingConstraintProof
- = RedPair { interpretation :: Interpretation }
+data DepGraphComponent =
+ DepGraphComponent { dgcRealScc :: Bool
+ , dgcDps :: DPS
+ , dgcDpProof :: DpProof
+ }
deriving ( Typeable )
+data OrderingConstraintProof = OCPRedPair RedPair
+ deriving ( Typeable )
+
+data RedPair = RPInterpretation Interpretation
+ | RPPathOrder PathOrder
+ deriving ( Typeable )
+
data Interpretation =
Interpretation { interpretation_type :: Interpretation_Type
, interprets :: [ Interpret ]
@@ -98,11 +122,12 @@
| Tropical Domain
deriving ( Typeable )
-data Interpret = forall s . XmlContent s => Interpret
- { symbol :: s , arity :: Int , value :: Value }
+data Interpret = Interpret
+ { symbol :: Symbol , arity :: Int , value :: Value }
deriving ( Typeable )
-data Value = Polynomial Polynomial
+data Value = Polynomial Polynomial
+ | ArithFunction ArithFunction
deriving ( Typeable )
data Polynomial = Sum [ Polynomial ]
@@ -111,6 +136,24 @@
| Polynomial_Variable String
deriving ( Typeable )
+data ArithFunction = AFNatural Integer
+ | AFVariable Integer
+ | AFSum [ArithFunction]
+ | AFProduct [ArithFunction]
+ | AFMin [ArithFunction]
+ | AFMax [ArithFunction]
+ | AFIfEqual ArithFunction ArithFunction ArithFunction ArithFunction
+ deriving ( Typeable )
+
+data Symbol = SymName Identifier
+ | SymSharp Symbol
+ | SymLabel Symbol Label
+ deriving ( Typeable )
+
+data Label = LblNumber [Integer]
+ | LblSymbol [Symbol]
+ deriving ( Typeable )
+
data Coefficient = Vector [ Coefficient ]
| Matrix [ Coefficient ]
| forall a . XmlContent a => Coefficient_Coefficient a
@@ -121,3 +164,18 @@
class ToExotic a where toExotic :: a -> Exotic
+data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
+ deriving Typeable
+
+data PrecedenceEntry = PrecedenceEntry { peSymbol :: Symbol
+ , peArity :: Int
+ , pePrecedence :: Integer
+ }
+ deriving Typeable
+
+data ArgumentFilterEntry =
+ ArgumentFilterEntry { afeSymbol :: Symbol
+ , afeArity :: Int
+ , afeFilter :: Either Int [Int]
+ }
+ deriving Typeable
diff --git a/TPDB/CPF/Proof/Util.hs b/TPDB/CPF/Proof/Util.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/CPF/Proof/Util.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE LambdaCase #-}
+module TPDB.CPF.Proof.Util where
+
+import qualified Data.Map as M
+import Data.List (nub)
+import TPDB.Data
+import TPDB.CPF.Proof.Type hiding (name)
+import TPDB.DP
+
+fromMarkedIdentifier :: Marked Identifier -> Symbol
+fromMarkedIdentifier = \case
+ Original i -> SymName i
+ Marked i -> SymSharp $ SymName i
+
+sortVariables :: Rule (Term Identifier s) -> Rule (Term Identifier s)
+sortVariables r = r { lhs = vmap mapVar $ lhs r
+ , rhs = vmap mapVar $ rhs r
+ }
+ where
+ oldVars = nub $ voccs $ lhs r
+ newVars = zipWith mkNewVar [1..] oldVars
+ mkNewVar i v = v { name = "x" ++ show i }
+ mapping = M.fromList $ zip oldVars newVars
+ mapVar v = case M.lookup v mapping of
+ Just v' -> v'
+ Nothing -> error "TPDB.CPF.Proof.Util.sortVariables"
diff --git a/TPDB/CPF/Proof/Write.hs b/TPDB/CPF/Proof/Write.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/CPF/Proof/Write.hs
@@ -0,0 +1,323 @@
+{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}
+
+-- | from internal representation to XML, and back
+
+module TPDB.CPF.Proof.Write where
+
+import TPDB.CPF.Proof.Type
+import qualified TPDB.Data as T
+
+import qualified Text.XML.HaXml.Escape as E
+import qualified Text.XML.HaXml.Pretty as P
+
+import Text.XML.HaXml.Types (QName (..) )
+import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
+import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..) )
+
+import TPDB.Xml
+import TPDB.Data.Xml
+
+import Data.List ( nub )
+import Data.Char ( toLower )
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import qualified Data.Time as T
+import Control.Monad
+import Data.Typeable
+import Data.Ratio
+
+tox :: CertificationProblem -> Document ()
+tox p =
+ let xd = XMLDecl "1.0" ( Just $ EncodingDecl "UTF-8" ) Nothing
+ pro = Prolog ( Just xd ) [] Nothing []
+ [ CElem e _ ] = toContents p
+ in Document pro emptyST e []
+
+instance XmlContent CertificationProblem where
+ parseContents = error "parseContents not implemented"
+
+ toContents cp = rmkel "certificationProblem"
+ [ mkel "input" $ toContents ( input cp )
+ , mkel "cpfVersion" [ nospaceString $ cpfVersion cp ]
+ , mkel "proof" $ toContents ( proof cp )
+ , mkel "origin" $ toContents ( origin cp )
+ ]
+
+instance XmlContent Origin where
+ parseContents = error "parseContents not implemented"
+
+ toContents o = case o of
+ ProofOrigin t -> rmkel "proofOrigin" $ toContents t
+
+instance XmlContent Tool where
+ parseContents = error "parseContents not implemented"
+
+ toContents t = rmkel "tool"
+ [ mkel "name" [ nospaceString $ name t ]
+ , mkel "version" [ nospaceString $ version t ]
+ ]
+
+instance XmlContent CertificationProblemInput where
+ parseContents = error "parseContents not implemented"
+
+ toContents i = case i of
+ TrsInput {} -> rmkel "trsInput" $ toContents ( symbolize $ trsinput_trs i )
+
+instance XmlContent ( T.TRS Identifier Symbol ) where
+ parseContents = error "parseContents not implemented"
+
+ toContents s = rmkel "trs"
+ $ rmkel "rules" $ concat $ map toContents $ T.rules s
+
+instance ( Typeable t, XmlContent t )
+ => XmlContent ( T.Rule t) where
+ parseContents = error "parseContents not implemented"
+
+ toContents u = rmkel "rule" $ concat
+ [ rmkel "lhs" ( toContents $ T.lhs u )
+ , rmkel "rhs" ( toContents $ T.rhs u )
+ ]
+
+instance XmlContent Proof where
+ parseContents = error "parseContents not implemented"
+
+ toContents p = case p of
+ TrsTerminationProof p -> toContents p
+
+instance XmlContent DPS where
+ parseContents = error "parseContents not implemented"
+
+ toContents ( DPS rules ) = rmkel "dps"
+ $ rmkel "rules" $ rules >>= toContents
+
+instance XmlContent TrsTerminationProof where
+ parseContents = error "parseContents not implemented"
+
+ toContents p = rmkel "trsTerminationProof" $ case p of
+ RIsEmpty -> rmkel "rIsEmpty" []
+ DpTrans {} -> rmkel "dpTrans" $ concat
+ [ toContents $ dptrans_dps p
+ , rmkel "markedSymbols" [ nospaceString "true" ]
+ , toContents $ dptrans_dpProof p
+ ]
+ StringReversal {} -> rmkel "stringReversal" $ concat
+ [ toContents $ symbolize $ trs p
+ , toContents $ trsTerminationProof p
+ ]
+ RuleRemoval {} -> rmkel "ruleRemoval" $ concat
+ [ toContents $ rr_orderingConstraintProof p
+ , toContents $ symbolize $ trs p
+ , toContents $ trsTerminationProof p
+ ]
+
+symbolize trs =
+ ( fmap (fmap SymName) trs )
+ { T.signature = map SymName $ T.signature trs }
+
+instance XmlContent Model where
+ parseContents = error "parseContents not implemented"
+
+ toContents model = rmkel "model" $ case model of
+ FiniteModel carrierSize interprets ->
+ rmkel "finiteModel" $ concat
+ [ rmkel "carrierSize" [ nospaceString $ show carrierSize ]
+ , concatMap toContents interprets
+ ]
+
+instance XmlContent DpProof where
+ parseContents = error "parseContents not implemented"
+
+ toContents p = rmkel "dpProof" $ case p of
+ PIsEmpty -> rmkel "pIsEmpty" []
+ RedPairProc {} -> case rppUsableRules p of
+ Nothing -> rmkel "redPairProc" $ concat
+ [ toContents $ rppOrderingConstraintProof p
+ , toContents $ rppDps p
+ , toContents $ rppDpProof p
+ ]
+ Just (DPS ur) -> rmkel "redPairUrProc" $ concat
+ [ toContents $ rppOrderingConstraintProof p
+ , toContents $ rppDps p
+ , rmkel "usableRules" $ rmkel "rules" $ concatMap toContents ur
+ , toContents $ rppDpProof p
+ ]
+ DepGraphProc cs -> rmkel "depGraphProc" $ concat $ map toContents cs
+
+ SemLabProc {} -> rmkel "semlabProc" $ concat
+ [ toContents $ slpModel p
+ , toContents $ slpDps p
+ , case slpTrs p of
+ DPS rules -> rmkel "trs" $ rmkel "rules" $ rules >>= toContents
+
+ , toContents $ slpDpProof p
+ ]
+
+ UnlabProc {} -> rmkel "unlabProc" $ concat
+ [ toContents $ ulpDps p
+ , case ulpTrs p of
+ DPS rules -> rmkel "trs" $ rmkel "rules" $ rules >>= toContents
+ , toContents $ ulpDpProof p
+ ]
+
+instance XmlContent DepGraphComponent where
+ toContents dgc = rmkel "component" $ concat $
+ [ {- rmkel "dps" $ -} toContents $ dgcDps dgc
+ , rmkel "realScc"
+ -- $ toContents $ dgcRealScc dgc
+ -- NO, Bool is encoded as text, not as attribute
+ [ nospaceString $ map toLower $ show $ dgcRealScc dgc ]
+ ] ++
+ [ {- rmkel "dpProof" $ -} toContents $ dgcDpProof dgc
+ | dgcRealScc dgc
+ ]
+
+instance XmlContent OrderingConstraintProof where
+ parseContents = error "parseContents not implemented"
+
+ toContents (OCPRedPair rp) = rmkel "orderingConstraintProof"
+ $ toContents rp
+
+instance XmlContent RedPair where
+ parseContents = error "parseContents not implemented"
+
+ toContents rp = rmkel "redPair" $ case rp of
+ RPInterpretation i -> toContents i
+ RPPathOrder o -> toContents o
+
+instance XmlContent Interpretation where
+ parseContents = error "parseContents not implemented"
+
+ toContents i = rmkel "interpretation" $
+ rmkel "type" ( toContents $ interpretation_type i )
+ ++ concatMap toContents ( interprets i )
+
+instance XmlContent Interpretation_Type where
+ parseContents = error "parseContents not implemented"
+
+ toContents t = rmkel "matrixInterpretation" $ concat
+ [ toContents ( domain t )
+ , rmkel "dimension" [ nospaceString $ show $ dimension t ]
+ , rmkel "strictDimension" [ nospaceString $ show $ strictDimension t ]
+ ]
+
+instance XmlContent Domain where
+ parseContents = error "parseContents not implemented"
+
+ toContents d = rmkel "domain" $ case d of
+ Naturals -> rmkel "naturals" []
+ Rationals delta -> rmkel "rationals"
+ $ rmkel "delta" $ toContents delta
+ Arctic d -> rmkel "arctic" $ toContents d
+ Tropical d -> rmkel "tropical" $ toContents d
+
+instance XmlContent Rational where
+ parseContents = error "parseContents not implemented"
+
+ toContents r = rmkel "rational"
+ [ mkel "numerator" [ nospaceString $ show $ numerator r ]
+ , mkel "denominator" [ nospaceString $ show $ denominator r ]
+ ]
+
+instance XmlContent Interpret where
+ parseContents = error "parseContents not implemented"
+
+ toContents i = rmkel "interpret" $ concat
+ [ toContents $ symbol i
+ , rmkel "arity" [ nospaceString $ show $ arity i ]
+ , toContents $ value i
+ ]
+
+instance XmlContent Value where
+ parseContents = error "parseContents not implemented"
+
+ toContents v = case v of
+ Polynomial p -> toContents p
+ ArithFunction f -> toContents f
+
+instance XmlContent Polynomial where
+ parseContents = error "parseContents not implemented"
+
+ toContents p = rmkel "polynomial" $ case p of
+ Sum ps -> rmkel "sum" $ concat ( map toContents ps )
+ Product ps -> rmkel "product" $ concat ( map toContents ps )
+ Polynomial_Coefficient c -> rmkel "coefficient" $ toContents c
+ Polynomial_Variable v -> rmkel "variable" [ nospaceString v ]
+
+instance XmlContent ArithFunction where
+ parseContents = error "parseContents not implemented"
+
+ toContents af = rmkel "arithFunction" $ case af of
+ AFNatural n -> rmkel "natural" [ nospaceString $ show n ]
+ AFVariable n -> rmkel "variable" [ nospaceString $ show n ]
+ AFSum afs -> rmkel "sum" $ concatMap toContents afs
+ AFProduct afs -> rmkel "product" $ concatMap toContents afs
+ AFMin afs -> rmkel "min" $ concatMap toContents afs
+ AFMax afs -> rmkel "max" $ concatMap toContents afs
+ AFIfEqual a b t f -> rmkel "ifEqual" $ concatMap toContents [a,b,t,f]
+
+instance XmlContent Coefficient where
+ parseContents = error "parseContents not implemented"
+
+ toContents v = case v of
+ Matrix vs -> rmkel "matrix" $ concat ( map toContents vs )
+ Vector cs -> rmkel "vector" $ concat ( map toContents cs )
+ Coefficient_Coefficient i ->
+ rmkel "coefficient" $ toContents i
+
+instance XmlContent Exotic where
+ parseContents = error "parseContents not implemented"
+
+ toContents e = case e of
+ Minus_Infinite -> rmkel "minusInfinity" []
+ E_Integer i -> rmkel "integer" [ nospaceString $ show i ]
+ Plus_Infinite -> rmkel "plusInfinity" []
+
+-- see remark in TPDB.Data.Xml (sharp_name_HACK)
+
+instance XmlContent Symbol where
+ parseContents = error "parseContents not implemented"
+
+ toContents (SymName id) = rmkel "name" [nospaceString $ show id]
+ toContents (SymSharp sym) = rmkel "sharp" $ toContents sym
+ toContents (SymLabel sym label) = rmkel "labeledSymbol"
+ $ toContents sym ++ (toContents label)
+
+instance XmlContent Label where
+ parseContents = error "parseContents not implemented"
+
+ toContents (LblNumber is) =
+ rmkel "numberLabel" $ map (\i -> mkel "number" [ nospaceString $ show i ]) is
+
+ toContents (LblSymbol ss) = rmkel "symbolLabel" $ concatMap toContents ss
+
+instance XmlContent PathOrder where
+ parseContents = error "parseContents not implemented"
+
+ toContents (PathOrder ps as) = rmkel "pathOrder" $ concat
+ [ rmkel "statusPrecedence" $ concatMap toContents ps
+ , if null as then []
+ else rmkel "argumentFilter" $ concatMap toContents as
+ ]
+
+instance XmlContent PrecedenceEntry where
+ parseContents = error "parseContents not implemented"
+
+ toContents (PrecedenceEntry s a p) = rmkel "statusPrecedenceEntry" $ concat
+ [ toContents s
+ , rmkel "arity" [ nospaceString $ show a ]
+ , rmkel "precedence" [ nospaceString $ show p ]
+ , rmkel "lex" [ ]
+ ]
+
+instance XmlContent ArgumentFilterEntry where
+ parseContents = error "parseContents not implemented"
+
+ toContents (ArgumentFilterEntry s a f) = rmkel "argumentFilterEntry" $ concat
+ [ toContents s
+ , rmkel "arity" [ nospaceString $ show a ]
+ , case f of
+ Left i -> rmkel "collapsing" [ nospaceString $ show i ]
+ Right is -> rmkel "nonCollapsing"
+ $ map (\i -> mkel "position" [ nospaceString $ show i ]) is
+ ]
diff --git a/TPDB/CPF/Proof/Xml.hs b/TPDB/CPF/Proof/Xml.hs
--- a/TPDB/CPF/Proof/Xml.hs
+++ b/TPDB/CPF/Proof/Xml.hs
@@ -1,172 +1,6 @@
-{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}
-
--- | from internal representation to XML, and back
-
-module TPDB.CPF.Proof.Xml where
-
-import TPDB.CPF.Proof.Type
-import qualified TPDB.Data as T
-
-import qualified Text.XML.HaXml.Escape as E
-import qualified Text.XML.HaXml.Pretty as P
-
-import Text.XML.HaXml.Types (QName (..) )
-import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
-import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..) )
-
-import TPDB.Xml
-import TPDB.Data.Xml
-
-import Data.List ( nub )
-import Data.Char ( toLower )
-import Data.Map (Map)
-import qualified Data.Map as Map
-
-import qualified Data.Time as T
-import Control.Monad
-import Data.Typeable
-import Data.Ratio
-
-tox :: CertificationProblem -> Document ()
-tox p =
- let xd = XMLDecl "1.0" ( Just $ EncodingDecl "UTF-8" ) Nothing
- pro = Prolog ( Just xd ) [] Nothing []
- [ CElem e _ ] = toContents p
- in Document pro emptyST e []
-
-instance XmlContent CertificationProblem where
- toContents cp = rmkel "certificationProblem"
- [ mkel "input" $ toContents ( input cp )
- , mkel "cpfVersion" [ CString False ( cpfVersion cp ) () ]
- , mkel "proof" $ toContents ( proof cp )
- , mkel "origin" $ toContents ( origin cp )
- ]
-
-instance XmlContent Origin where
- toContents o = case o of
- ProofOrigin t -> rmkel "proofOrigin" $ toContents t
-
-instance XmlContent Tool where
- toContents t = rmkel "tool"
- [ mkel "name" [ CString False ( name t ) () ]
- , mkel "version" [ CString False ( version t ) () ]
- ]
-
-instance XmlContent CertificationProblemInput where
- toContents i = case i of
- TrsInput {} -> rmkel "trsInput" $ toContents ( trsinput_trs i )
-
-instance ( Typeable v, Typeable c, XmlContent v , XmlContent c )
- => XmlContent ( T.TRS v c ) where
- toContents s = rmkel "trs"
- $ rmkel "rules" $ concat $ map toContents $ T.rules s
-
-instance ( Typeable t, XmlContent t )
- => XmlContent ( T.Rule t) where
- toContents u = rmkel "rule" $
- rmkel "lhs" ( toContents $ T.lhs u )
- ++ rmkel "rhs" ( toContents $ T.rhs u )
-
-
-instance XmlContent Proof where
- toContents p = case p of
- TrsTerminationProof p -> toContents p
-
-instance ( Typeable i , XmlContent i ) => XmlContent ( Sharp i ) where
- toContents s = case s of
- Plain p -> toContents p
- Sharp q -> rmkel "sharp" $ toContents q
-
-instance XmlContent DPS where
- toContents ( DPS rules ) = rmkel "dps"
- $ rmkel "rules" $ rules >>= toContents
-
-instance XmlContent TrsTerminationProof where
- toContents p = rmkel "trsTerminationProof" $ case p of
- RIsEmpty -> rmkel "rIsEmpty" []
- DpTrans {} -> rmkel "dpTrans" $
- toContents ( dptrans_dps p )
- ++ rmkel "markedSymbols" [ CString False "true" () ]
- ++ toContents ( dptrans_dpProof p )
- StringReversal {} -> rmkel "stringReversal" $
- ( toContents $ trs p )
- ++ ( toContents $ trsTerminationProof p )
- RuleRemoval {} -> rmkel "ruleRemoval"
- $ toContents ( rr_orderingConstraintProof p )
- ++ toContents ( trs p )
- ++ toContents ( trsTerminationProof p )
-
-instance XmlContent DpProof where
- toContents p = rmkel "dpProof" $ case p of
- PIsEmpty -> rmkel "pIsEmpty" []
- RedPairProc {} -> rmkel "redPairProc"
- $ toContents ( dp_orderingConstraintProof p )
- ++ toContents ( red_pair_dps p )
- ++ toContents ( redpairproc_dpProof p )
-
-instance XmlContent OrderingConstraintProof where
- toContents p = rmkel "orderingConstraintProof" $ case p of
- RedPair {} -> rmkel "redPair" $ toContents ( interpretation p )
-
-instance XmlContent Interpretation where
- toContents i = rmkel "interpretation" $
- rmkel "type" ( toContents $ interpretation_type i )
- ++ concat ( map toContents $ interprets i )
-
-instance XmlContent Interpretation_Type where
- toContents t = rmkel "matrixInterpretation" $
- toContents ( domain t )
- ++ rmkel "dimension"
- [ CString False ( show ( dimension t )) () ]
- ++ rmkel "strictDimension"
- [ CString False ( show ( strictDimension t )) () ]
-
-instance XmlContent Domain where
- toContents d = rmkel "domain" $ case d of
- Naturals -> rmkel "naturals" []
- Rationals delta -> rmkel "rationals"
- $ rmkel "delta" $ toContents delta
- Arctic d -> rmkel "arctic" $ toContents d
- Tropical d -> rmkel "tropical" $ toContents d
-
-instance XmlContent Rational where
- toContents r = rmkel "rational"
- [ mkel "numerator" [ CString False ( show $ numerator r ) () ]
- , mkel "denominator" [ CString False ( show $ denominator r ) () ]
- ]
-
-instance XmlContent Interpret where
- toContents i = rmkel "interpret" $ case i of
- Interpret { symbol = s } ->
- sharp_name_HACK ( toContents s )
- ++ rmkel "arity" [ CString False ( show ( arity i )) () ]
- ++ toContents ( value i )
-
-instance XmlContent Value where
- toContents v = case v of
- Polynomial p -> toContents p
-
-instance XmlContent Polynomial where
- toContents p = rmkel "polynomial" $ case p of
- Sum ps -> rmkel "sum" $ concat ( map toContents ps )
- Product ps -> rmkel "product" $ concat ( map toContents ps )
- Polynomial_Coefficient c -> rmkel "coefficient" $ toContents c
- Polynomial_Variable v -> rmkel "variable" [ CString False v () ]
-
-
-instance XmlContent Coefficient where
- toContents v = case v of
- Matrix vs -> rmkel "matrix" $ concat ( map toContents vs )
- Vector cs -> rmkel "vector" $ concat ( map toContents cs )
- Coefficient_Coefficient i ->
- rmkel "coefficient" $ toContents i
-
-instance XmlContent Exotic where
- toContents e = case e of
- Minus_Infinite -> rmkel "minusInfinity" []
- E_Integer i -> rmkel "integer" [ CString False ( show i ) () ]
- Plus_Infinite -> rmkel "plusInfinity" []
-
-
-
-
+module TPDB.CPF.Proof.Xml
+( module TPDB.CPF.Proof.Read
+, module TPDB.CPF.Proof.Write
+) where
+import TPDB.CPF.Proof.Read
+import TPDB.CPF.Proof.Write
diff --git a/TPDB/DP.hs b/TPDB/DP.hs
--- a/TPDB/DP.hs
+++ b/TPDB/DP.hs
@@ -1,52 +1,7 @@
-{-# language OverloadedStrings #-}
-
-module TPDB.DP where
-
-import TPDB.Data
-import TPDB.Pretty
-import TPDB.Pretty
-
-import qualified Data.Set as S
-import Control.Monad ( guard )
-
-import Data.Hashable
-import GHC.Generics
-
-data Marked a = Original a | Marked a | Auxiliary a
- deriving ( Eq, Ord )
+module TPDB.DP ( module TPDB.DP.Transform )
-instance Hashable a => Hashable (Marked a) where
- hashWithSalt s m = case m of
- Original x -> hashWithSalt s $ hashWithSalt (0::Int) x
- Marked x -> hashWithSalt s $ hashWithSalt (1::Int) x
- Auxiliary x -> hashWithSalt s $ hashWithSalt (2::Int) x
+where
-instance Pretty a => Pretty ( Marked a) where
- pretty m = case m of
- Original a -> pretty a
- Marked a -> pretty a <> "#"
- Auxiliary a -> pretty a
+import TPDB.DP.Transform
+import TPDB.DP.Graph
-dp s =
- let marked (Node f args) =
- Node (Marked f) $ map (fmap Original) args
- os = map ( \ u -> Rule { relation = Weak
- , lhs = fmap Original $ lhs u
- , rhs = fmap Original $ rhs u
- , top = False
- } )
- $ rules s
- defined = S.fromList $ do
- u <- rules s
- let Node f args = lhs u
- return f
- us = do
- u <- rules s
- (_, r @ (Node f args)) <- positions $ rhs u
- guard $ S.member f defined
- return $ Rule { relation = Strict
- , lhs = marked $ lhs u
- , rhs = marked r
- , top = True
- }
- in RS { rules = us ++ os, separate = separate s }
diff --git a/TPDB/DP/Graph.hs b/TPDB/DP/Graph.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/DP/Graph.hs
@@ -0,0 +1,53 @@
+module TPDB.DP.Graph where
+
+import TPDB.DP.TCap
+import TPDB.DP.Unify
+import TPDB.DP.Transform
+
+import TPDB.Data
+import TPDB.Pretty
+
+import TPDB.Plain.Read -- for testing
+import TPDB.Plain.Write -- for testing
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+import Data.Graph ( stronglyConnComp, SCC(..) )
+import Control.Monad ( guard, forM )
+import Control.Applicative
+
+import Control.Monad.State.Strict
+
+
+-- | DP problems for strongly connected components,
+-- topologically sorted, with CyclicComponents in Right,
+-- others in Left.
+components s = do
+ let es = M.fromListWith (++)
+ $ do (p,q) <- edges s ; return (p, [q])
+ key = M.fromList
+ $ zip (filter strict $ rules s) [0.. ]
+ comp <- reverse $ stronglyConnComp $ do
+ p <- M.keys key
+ let qs = M.findWithDefault [] p es
+ return (p, key M.! p, map (key M.!) qs )
+ return $ case comp of
+ CyclicSCC vs -> Right $ s { rules = vs
+ ++ filter (not . strict) (rules s) }
+ AcyclicSCC v -> Left v
+
+-- | edges of the estimated dependency graph
+edges s = do
+ let def = S.filter isOriginal $ defined s
+ u <- filter strict $ rules s
+ v <- filter strict $ rules s
+ guard $ unifies ( vmap Left $ tcap s $ rhs u )
+ ( vmap Right $ lhs v )
+ return (u,v)
+
+check = edges $ dp sys
+
+-- example from "DP Revisited" http://colo6-c703.uibk.ac.at/ttt/rta04.pdf
+Right sys =
+ TPDB.Plain.Read.trs "(VAR x y) (RULES not(not(x)) -> x not(or(x,y)) -> and(not(x),not(y)) not(and(x,y)) -> or (not(x),not(y)) and(x,or(y,z)) -> or(and(x,z),and(y,z)) and(or(y,z),x) -> or(and(x,y),and(x,z)))"
+
diff --git a/TPDB/DP/TCap.hs b/TPDB/DP/TCap.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/DP/TCap.hs
@@ -0,0 +1,29 @@
+module TPDB.DP.TCap where
+
+import TPDB.Data
+import TPDB.Pretty
+
+import TPDB.DP.Unify
+
+import Control.Monad.State.Strict
+import Control.Applicative
+
+
+-- | This function keeps only those parts of the input term which cannot be reduced,
+-- even if the term is instantiated. All other parts are replaced by fresh variables.
+-- Def 4.4 in http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf
+
+tcap :: (Ord v, Ord c) => TRS v c -> Term v c -> Term Int c
+tcap dp t = evalState ( walk dp t ) 0
+
+fresh_var :: State Int ( Term Int c )
+fresh_var = do i <- get ; put $ succ i ; return $ Var i
+
+walk dp t = case t of
+ Node f args -> do
+ t' <- Node f <$> forM args (walk dp)
+ if all ( \ u -> not $ unifies ( vmap Left $ lhs u ) ( vmap Right t' ) )
+ $ filter (not . strict) $ rules dp
+ then return t' else fresh_var
+ _ -> fresh_var
+
diff --git a/TPDB/DP/Transform.hs b/TPDB/DP/Transform.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/DP/Transform.hs
@@ -0,0 +1,71 @@
+{-# language OverloadedStrings #-}
+{-# LANGUAGE DeriveGeneric #-}
+
+module TPDB.DP.Transform where
+
+import TPDB.Data
+import TPDB.Pretty
+
+import qualified Data.Set as S
+import Control.Monad ( guard, forM )
+
+import Data.Hashable
+import GHC.Generics
+
+data Marked a = Original a | Marked a | Auxiliary a
+ deriving ( Show, Eq, Ord, Generic )
+
+isOriginal m = case m of Original {} -> True ; _ -> False
+isMarked m = case m of Marked {} -> True ; _ -> False
+
+instance Hashable a => Hashable (Marked a)
+
+instance Pretty a => Pretty ( Marked a) where
+ pretty m = case m of
+ Original a -> pretty a
+ Marked a -> pretty a <> "#"
+ Auxiliary a -> pretty a
+
+mark_top :: Term v a -> Term v (Marked a)
+mark_top (Node f args) =
+ Node (Marked f) $ map (fmap Original) args
+
+defined s = S.fromList $ do
+ u <- rules s
+ let Node f args = lhs u
+ -- will raise exception if lhs is variable
+ return f
+
+-- | compute the DP transformed system.
+
+dp :: (Ord v, Ord s)
+ => RS s (Term v s)
+ -> RS (Marked s) (Term v (Marked s))
+dp s =
+ let os = map ( \ u -> Rule { relation = Weak
+ , lhs = fmap Original $ lhs u
+ , rhs = fmap Original $ rhs u
+ , top = False
+ } )
+ $ rules s
+ def = defined s
+ us = do
+ u <- rules s
+ let ssubs = S.fromList $ strict_subterms $ lhs u
+ walk r = if S.member r ssubs then [] else case r of
+ -- will raise exception if rhs contains
+ -- a variable that is not in lhs
+ Node f args ->
+ ( if S.member f def then (r :) else id )
+ ( args >>= walk )
+ r <- walk $ rhs u
+ return $ Rule { relation = Strict
+ , lhs = mark_top $ lhs u
+ , rhs = mark_top r
+ , top = True
+ }
+ in RS { signature = map Marked ( S.toList def )
+ ++ map Original ( signature s )
+ , rules = us ++ os
+ , separate = separate s
+ }
diff --git a/TPDB/DP/Unify.hs b/TPDB/DP/Unify.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/DP/Unify.hs
@@ -0,0 +1,38 @@
+module TPDB.DP.Unify ( mgu, unifies, apply, times ) where
+
+import TPDB.Data
+import qualified Data.Map as M
+import Control.Monad ( guard, foldM )
+import Data.Maybe (isJust)
+
+type Substitution v c = M.Map v (Term v c)
+
+unifies t1 t2 = isJust $ mgu t1 t2
+
+-- | naive implementation (worst case exponential)
+mgu
+ :: (Ord v, Eq c) =>
+ Term v c -> Term v c -> Maybe (M.Map v (Term v c))
+mgu t1 t2 | t1 == t2 = return M.empty
+mgu ( Var v ) t2 = do
+ guard $ not $ elem (Var v) $ subterms t2
+ return $ M.singleton v t2
+mgu t1 ( Var v ) = mgu ( Var v ) t1
+mgu (Node f1 args1) (Node f2 args2)
+ | f1 == f2 && length args1 == length args2 = do
+ guard $ f1 == f2
+ foldM ( \ s (l,r) -> do
+ t <- mgu (apply l s) (apply r s)
+ return $ times s t ) M.empty $ zip args1 args2
+mgu _ _ = Nothing
+
+times :: Ord v
+ => Substitution v c -> Substitution v c -> Substitution v c
+times s t =
+ M.union ( M.difference t s )
+ ( M.map ( \ v -> apply v t ) s )
+
+apply t s = case t of
+ Var v -> case M.lookup v s of Nothing -> t ; Just w -> w
+ Node f args -> Node f $ map (\ a -> apply a s) args
+
diff --git a/TPDB/DP/Usable.hs b/TPDB/DP/Usable.hs
new file mode 100644
--- /dev/null
+++ b/TPDB/DP/Usable.hs
@@ -0,0 +1,43 @@
+module TPDB.DP.Usable where
+
+import TPDB.Data
+import TPDB.Pretty
+
+import TPDB.DP.Unify
+import TPDB.DP.TCap
+
+import qualified Data.Set as S
+
+-- | DANGER: this ignores the CE condition
+restrict :: (Ord c, Ord v) => RS c (Term v c) -> RS c (Term v c)
+restrict dp =
+ dp { rules = filter strict (rules dp)
+ ++ S.toList ( usable dp)
+ }
+
+-- | computes the least closed set of usable rules, cf. Def 4.5
+-- http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf
+
+usable :: (Ord v, Ord c)
+ => TRS v c -> S.Set (Rule (Term v c))
+usable dp = fixpoint ( \ s -> S.union s $ required dp s)
+ (required dp $ S.filter strict
+ $ S.fromList $ rules dp)
+
+fixpoint f x =
+ let y = f x in if x == y then x else fixpoint f y
+
+required :: (Ord v, Ord c)
+ => TRS v c -> S.Set ( Rule (Term v c) ) -> S.Set ( Rule (Term v c) )
+required dp rs =
+ S.fromList $ do { r <- S.toList rs ; needed dp $ rhs r }
+
+needed :: (Ord v, Ord c)
+ => TRS v c -> Term v c -> [ Rule (Term v c) ]
+needed dp t = case t of
+ Node f args ->
+ filter ( \ u -> unifies ( vmap Left $ lhs u ) ( vmap Right $ tcap dp t ) )
+ ( filter (not . strict) $ rules dp )
+ ++ ( args >>= needed dp )
+ Var v -> []
+
diff --git a/TPDB/Data.hs b/TPDB/Data.hs
--- a/TPDB/Data.hs
+++ b/TPDB/Data.hs
@@ -15,6 +15,7 @@
import Control.Monad ( guard )
import Data.Hashable
+import Data.Function (on)
data Identifier =
Identifier { _identifier_hash :: Int
@@ -30,6 +31,7 @@
mk a n = Identifier { _identifier_hash = hash (a,n)
, arity = a, name = n }
+
---------------------------------------------------------------------
data Relation = Strict | Weak | Equal deriving ( Eq, Ord, Typeable, Show )
@@ -49,13 +51,21 @@
equal :: Rule a -> Bool
equal u = case relation u of Equal -> True ; _ -> False
+instance Functor (RS s) where
+ fmap f rs = rs { rules = map (fmap f) $ rules rs }
+instance Functor Rule where
+ fmap f u = u { lhs = f $ lhs u, rhs = f $ rhs u }
+
data RS s r =
RS { signature :: [ s ] -- ^ better keep order in signature (?)
, rules :: [ Rule r ]
, separate :: Bool -- ^ if True, write comma between rules
}
deriving ( Typeable )
+
+instance Eq r => Eq (RS s r) where
+ (==) = (==) `on` rules
strict_rules sys =
do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
diff --git a/TPDB/Data/Term.hs b/TPDB/Data/Term.hs
--- a/TPDB/Data/Term.hs
+++ b/TPDB/Data/Term.hs
@@ -68,6 +68,18 @@
subterms arg
_ -> []
+-- Note: following implementation relies on @subterms@
+-- returning the preorder list (where the full term goes first)
+strict_subterms t = tail $ subterms t
+
+isSubtermOf :: (Eq v, Eq c )
+ => Term v c -> Term v c -> Bool
+isSubtermOf s t = elem s $ subterms t
+
+isStrictSubtermOf :: (Eq v, Eq c )
+ => Term v c -> Term v c -> Bool
+isStrictSubtermOf s t = elem s $ strict_subterms t
+
-- | compute new symbol at position, giving the position
pmap:: ( Position -> c -> d )
-> Term v c
diff --git a/TPDB/Data/Xml.hs b/TPDB/Data/Xml.hs
--- a/TPDB/Data/Xml.hs
+++ b/TPDB/Data/Xml.hs
@@ -37,10 +37,25 @@
: map ( \ x -> mkel "arg" $ toContents x ) xs
-}
-- for CPF:
+
+-- the problem is this:
+-- a variable is an Identifier, and must look like "foo"
+-- a constructor symbol is also an Identifier
+-- but it must look like "bar..."
+-- so it should be wrapped into
+-- but no, if the constructor is sharped (or labelled)
+-- then it must look like "bar..."
+-- price question: what is the correct
+-- instance XmlContent Identifier ?
+-- the answer probably is "there is none",
+-- and toContents (Term v Identifier) should never occur,
+-- instead need to call toContents (Term v Symbol)
+
toContents ( Node f args ) = rmkel "funapp"
- $ sharp_name_HACK ( toContents f )
+ $ no_sharp_name_HACK ( toContents f )
++ map ( \ arg -> mkel "arg" $ toContents arg ) args
+no_sharp_name_HACK e = e
sharp_name_HACK e = case e of
[ CElem ( Elem (N "sharp") [] cs ) () ] ->
diff --git a/TPDB/Input.hs b/TPDB/Input.hs
--- a/TPDB/Input.hs
+++ b/TPDB/Input.hs
@@ -5,10 +5,12 @@
import TPDB.XTC.Read
import TPDB.Convert
-import System.FilePath.Posix ( splitExtension )
+import System.FilePath.Posix ( takeExtension )
-- | read input from file with given name.
-- can have extension .srs, .trs, .xml.
+-- unknown extension is considered as .xml, because of
+-- http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks
get :: FilePath
-> IO ( Either (TRS Identifier Identifier)
@@ -19,9 +21,7 @@
Right x -> return x
Left err -> error err
-getE f = do
- let ( base, ext ) = splitExtension f
- case ext of
+getE f = case takeExtension f of
".srs" -> do
s <- readFile f
case srs s of
@@ -32,7 +32,7 @@
case TPDB.Plain.Read.trs s of
Left err -> return $ Left err
Right t -> return $ Right $ Left t
- ".xml" -> do
+ _ -> do
ps <- readProblems f
case ps of
[ p ] -> return $ Right $ Left $ TPDB.Data.trs p
diff --git a/TPDB/Pretty.hs b/TPDB/Pretty.hs
--- a/TPDB/Pretty.hs
+++ b/TPDB/Pretty.hs
@@ -53,3 +53,7 @@
Nothing -> text "Nothing"
Just x -> text "Just" <+> pretty x -- FIXME: parens missing
-}
+
+instance ( Pretty a, Pretty b ) => Pretty (Either a b) where
+ pretty (Left x) = text "Left" <+> parens (pretty x)
+ pretty (Right x) = text "Right" <+> parens (pretty x)
diff --git a/TPDB/Rainbow/Proof/Type.hs b/TPDB/Rainbow/Proof/Type.hs
deleted file mode 100644
--- a/TPDB/Rainbow/Proof/Type.hs
+++ /dev/null
@@ -1,176 +0,0 @@
-{-# language OverloadedStrings #-}
-{-# language ExistentialQuantification #-}
-{-# language DeriveDataTypeable #-}
-
--- | internal representation of Rainbow termination proofs,
--- see
--- this file is modelled after rainbow/proof.ml
--- it omits constructors not needed for matrix interpretations (for the moment)
-module TPDB.Rainbow.Proof.Type
-
-where
-
-import TPDB.Data hiding ( Type (..))
-import TPDB.Pretty
-import TPDB.Plain.Write () -- just instances
-
-import qualified TPDB.CPF.Proof.Type as C
-
-import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
-import qualified Text.Parsec as P
-
-import qualified Data.Time as T
-import Data.Typeable
-import Data.String (fromString)
-
-data Vector a = Vector [ a ]
- deriving Typeable
-
-data Matrix a = Matrix [ Vector a ]
- deriving Typeable
-
-data MaxPlus = MinusInfinite | MaxPlusFinite Integer
- deriving ( Show, Read, Typeable )
-
-data MinPlus = MinPlusFinite Integer | PlusInfinite
- deriving ( Show, Read, Typeable )
-
-data Mi_Fun a =
- Mi_Fun { mi_const :: Vector a
- , mi_args :: [ Matrix a ]
- }
- deriving Typeable
-
-data Poly_Fun a =
- Poly_Fun { coefficients :: [a]
- }
- deriving Typeable
-
-type Matrix_Int = Interpretation Mi_Fun
-type Polynomial_Int = Interpretation Poly_Fun
-
-data Interpretation f = forall k a
- . ( XmlContent k, XmlContent a, C.ToExotic a, Typeable a ) -- Haskell2Xml a
- =>
- Interpretation { mi_domain :: Domain
- , mi_dim :: Integer
- , mi_duration :: T.NominalDiffTime -- ^ this is an extension
- , mi_start :: T.UTCTime
- , mi_end :: T.UTCTime
- -- , mi_int :: [ (k , Mi_Fun a ) ]
- , mi_int :: [ (k , f a ) ]
- } deriving Typeable
-
-data Domain = Natural | Arctic | Arctic_Below_Zero | Tropical
- deriving ( Show, Eq, Ord, Typeable )
-
-instance Pretty Domain where pretty = fromString . show
-instance Pretty T.NominalDiffTime where pretty = fromString . show
-instance Pretty T.UTCTime where pretty = fromString . show
-
-data Red_Ord
- = Red_Ord_Matrix_Int Matrix_Int
- | Red_Ord_Polynomial_Int Polynomial_Int
- | Red_Ord_Simple_Projection Simple_Projection
- | Red_Ord_Usable_Rules Usable_Rules
- deriving Typeable
-
-data Usable_Rules = Usable_Rules [ Identifier ]
- deriving Typeable
-
-instance Pretty Usable_Rules where
- pretty (Usable_Rules sp) = "Usable_Rules" <+> pretty sp
-
-
-data Simple_Projection = Simple_Projection [ ( Identifier, Int ) ]
- deriving Typeable
-
-instance Pretty Simple_Projection where
- pretty (Simple_Projection sp) = "Simple_Projection" <+> pretty sp
-
-data Claim =
- Claim { system :: TRS Identifier Identifier
- , property :: Property
- }
- deriving Typeable
-
-data Proof =
- Proof { claim :: Claim
- , reason :: Reason
- }
- deriving Typeable
-
-data Property
- = Termination
- | Top_Termination
- | Complexity ( Function, Function )
- deriving ( Typeable )
-
-instance Show Property where show = render . pretty
-
-instance Pretty Property where
- pretty p = case p of
- Termination -> "YES # Termination"
- Top_Termination -> "YES # Top_Termination"
- Complexity ( lo, hi ) -> "YES" <+> pretty ( lo, hi )
-
--- | see specification:
--- http://termination-portal.org/wiki/Complexity
-data Function
- = Unknown
- | Polynomial { degree :: Maybe Int }
- | Exponential
- deriving ( Typeable )
-
-instance Show Function where show = render . pretty
-
-instance Pretty Function where
- pretty f = case f of
- Unknown -> "?"
- Polynomial { degree = Nothing } ->
- "POLY"
- Polynomial { degree = Just 0 } ->
- "O(1)"
- Polynomial { degree = Just d } ->
- "O" <+> parens ( "n^" <> pretty d)
-
-
-
-data Reason
- = Trivial
- | MannaNess Red_Ord Proof
- | MarkSymb Proof
- | DP Proof
- | Reverse Proof
- | As_TRS Proof
- | As_SRS Proof
- | SCC [ Proof ] -- ^ proposed extension
- | RFC Proof -- ^ experimental (not in Rainbow)
- | Undo_RFC Proof -- ^ experimental (not in Rainbow)
- | Bounded_Matrix_Interpretation Proof -- ^ TODO add more info
- deriving Typeable
-
-data Over_Graph = HDE | HDE_Marked
- deriving ( Show, Typeable )
-
-data Marked a = Hd_Mark a | Int_Mark a
- deriving ( Eq, Ord, Typeable )
-
-
-
-instance C.ToExotic Integer where
- toExotic = C.E_Integer
-instance C.ToExotic MaxPlus where
- toExotic a = case a of
- MinusInfinite -> C.Minus_Infinite
- MaxPlusFinite f -> C.E_Integer f
-instance C.ToExotic MinPlus where
- toExotic a = case a of
- MinPlusFinite f -> C.E_Integer f
- PlusInfinite -> C.Plus_Infinite
-
-{-
-instance C.ToExotic ( Xml_As_String Integer ) where
- toExotic ( Xml_As_String i ) = C.toExotic i
--}
-
diff --git a/TPDB/Rainbow/Proof/Xml.hs b/TPDB/Rainbow/Proof/Xml.hs
deleted file mode 100644
--- a/TPDB/Rainbow/Proof/Xml.hs
+++ /dev/null
@@ -1,290 +0,0 @@
-{-# language TypeSynonymInstances, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances, IncoherentInstances, PatternSignatures, DeriveDataTypeable #-}
-
--- | from internal representation to XML, and back
-
-module TPDB.Rainbow.Proof.Xml where
-
-import TPDB.Rainbow.Proof.Type
-
-import qualified TPDB.CPF.Proof.Type as C
-
-import TPDB.Xml
-import TPDB.Data.Xml
--- import Matrix.MaxPlus ( MaxPlus )
--- import Autolib.Reader hiding ( many )
--- import Autolib.TES
--- import Autolib.TES.Identifier ( mk, mknullary, mkunary )
-
-import TPDB.Data
-
-import qualified Text.XML.HaXml.Escape as E
-import qualified Text.XML.HaXml.Pretty as P
-
-import Text.XML.HaXml.Types (QName (..) )
-import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
-import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..) )
-
-import Data.List ( nub )
-import Data.Char ( toLower )
-import Data.Map (Map)
-import qualified Data.Map as Map
-
-import qualified Data.Time as T
-import Control.Monad
-import Data.Typeable
-
-tox :: Proof -> Document ()
-tox p =
- let xd = XMLDecl "1.0" ( Just $ EncodingDecl "ISO-8859-1" ) Nothing
- pro = Prolog ( Just xd ) [] Nothing []
- t = toplevel p
- et = E.xmlEscape E.stdXmlEscaper t
- -- don't escape, see remarks in Autolib.TES.Identifier
- in Document pro emptyST t []
-
-
-toplevel p =
- let atts = [ ( N "xmlns"
- , AttValue [ Left "urn:rainbow.proof.format" ]
- )
- , ( N "xmlns:xsi"
- , AttValue [ Left "http://www.w3.org/2001/XMLSchema-instance" ]
- )
- , ( N "xsi:schemaLocation"
- , AttValue [ Left "urn:rainbow.proof.format http://color.loria.fr/proof.xsd" ]
- )
- ]
- unProof [ CElem ( Elem (N "proof") [] cs ) _ ] = cs
- in Elem (N "proof") atts $ unProof $ toContents p
-
-
-instance ( Typeable a, XmlContent a ) => XmlContent ( Vector a ) where
- toContents ( Vector xs ) =
- map ( \ x -> mkel "velem" ( toContents x ) ) xs
- parseContents = wrap xread
-
-instance XRead a => XRead ( Vector a ) where
- xread = fmap Vector $ many $ element "velem" xread
-
-
--- FIXME:
-instance XmlContent MaxPlus where
- parseContents = do
- CString _ s _ <- next
- return $ read s
- toContents i =
- [ CString False ( escape $ show i ) () ]
-
-
--- | for some types, e.g. Integer
--- , do not use XmlContent instance for element type
--- but show them (as string).
--- reason: the XmlContent module contains an instance
--- for integer that produces
--- and there is no way to turn this off.
-
-data Xml_As_String a = Xml_As_String a
- deriving Typeable
-
-instance ( Typeable a, Show a, Read a ) => XmlContent (Xml_As_String a) where
- toContents ( Xml_As_String x ) = [ CString False ( show x ) () ]
- parseContents = wrap $ fmap Xml_As_String $ xfromstring
-
-instance ( Typeable a, XmlContent a )
- => XmlContent ( Matrix a ) where
- toContents ( Matrix xs ) =
- map ( \ x -> mkel "row" ( toContents x ) ) xs
- parseContents = wrap xread
-
-instance XRead a => XRead ( Matrix a ) where
- xread = do
- rs <- many $ element "row" xread
- return $ Matrix rs
-
-instance ( Typeable a, XmlContent a )
- => XmlContent ( Mi_Fun a ) where
- toContents ( Mi_Fun { mi_const = c, mi_args = xs } ) = return $
- mkel "mi_fun"
- $ mkel "const" ( toContents c )
- : map ( mkel "arg" . toContents ) xs
- parseContents = wrap xread
-
-instance XRead a => XRead ( Mi_Fun a ) where
- xread = element "mi_fun" $ do
- con <- element "const" xread
- args <- many $ element "arg" xread
- return $ Mi_Fun { mi_const = con, mi_args = args }
-
-instance C.ToExotic a => C.ToExotic (Xml_As_String a) where
- toExotic (Xml_As_String x) = C.toExotic x
-
---------------------------------------------------------------------------------
-
-instance XmlContent Domain where
- toContents d = [ CString False ( show d ) ( )]
-
-instance XmlContent Matrix_Int where
- toContents ( Interpretation { mi_domain = o, mi_dim = d, mi_int = i
- , mi_start = s, mi_end = e, mi_duration = u } ) =
- return $ mkel ( case o of Natural -> "matrix_int"
- Arctic -> "arctic_int"
- Arctic_Below_Zero -> "arctic_bz_int"
- Tropical -> "tropical_int" )
- [ mkel "dimension" [ CString False ( show d ) () ]
- , mkel "mi_map" $ do
- ( k, v ) <- i
- return $ mkel "mapping"
- $ mkel "fun" ( toContents k )
- : toContents v
- -- the following are not standard rainbow,
- -- so they have to come after the standard elements
- -- because the rainbow parser then ignores them
- , mkel "start" [ CString False ( show s ) () ]
- , mkel "end" [ CString False ( show e ) () ]
- , mkel "duration" [ CString False ( show u ) () ]
- ]
- parseContents = wrap xread
-
-instance XRead Matrix_Int where
- xread = foldr1 orelse
- [ mai "matrix_int" Natural ( undefined :: Xml_As_String Integer )
- , mai "arctic_int" Arctic ( undefined :: MaxPlus )
- , mai "arctic_bz_int" Arctic_Below_Zero ( undefined :: MaxPlus )
- ]
-
--- | FIXME this is broken because the keys could be
--- Identifier or Marked Identifier
-mai :: forall a . ( Typeable a, XmlContent a, C.ToExotic a )
- => String -> Domain -> a -> CParser Matrix_Int
-mai tag o v0 = element tag $ do
- d <- element "dimension" $ xfromstring
- i <- element "mi_map" $ many $ element "mapping" $ do
- k :: Identifier <- element "fun" $ xread -- FIXME
- v :: Mi_Fun a <- xread
- return ( k, v )
- s <- element "start" $ xfromstring
- e <- element "end" $ xfromstring
- let u = T.diffUTCTime e s
- return $ Interpretation
- { mi_domain = o, mi_dim = d, mi_int = i
- , mi_start = s, mi_end = e, mi_duration = u
- }
-
-instance XmlContent Red_Ord where
- toContents ro = case ro of
- Red_Ord_Matrix_Int mi -> return $
- mkel "order" $ toContents mi
- Red_Ord_Simple_Projection sp -> return $
- mkel "order" $ toContents sp
- parseContents = wrap xread
-
-instance XmlContent Simple_Projection where
- toContents ( Simple_Projection sp ) = return $
- mkel "simple_projection" $ map ( \ (f,i) ->
- mkel "project" [ mkel "symbol" $ toContents (Hd_Mark $ unP f)
- , mkel "position" $ toContents $ Xml_As_String i
- ]
- ) sp
- parseContents = wrap xread
-
-instance XRead Simple_Projection where
- xread = element "simple_projection"
- $ fmap Simple_Projection xread
-
-instance XRead Red_Ord where
- xread = element "order"
- $ orelse ( fmap Red_Ord_Matrix_Int xread )
- ( fmap Red_Ord_Simple_Projection xread )
-
-instance HTypeable Proof where
- toHType p = Prim "proof" "proof"
-
-
-instance XmlContent Proof where
- toContents p0 = let { p = reason p0 } in return $ mkel "proof" $ case p of
- Trivial -> return $ mkel "trivial" []
- MannaNess o p -> return
- $ mkel "manna_ness" $ toContents o ++ toContents p
- MarkSymb p -> return $ mkel "mark_symbols" $ toContents p
- DP p -> return $ mkel "dp" $ toContents p
- As_TRS p -> return $ mkel "as_trs" $ toContents p
- Reverse p -> return $ mkel "reverse" $ toContents p
- SCC parts -> return $ mkel "scc_decomp"
- $ mkel "graph" ( toContents HDE_Marked )
- : do
- p <- parts
- let sys = system $ claim p
- vs = signature sys
- u = head $ filter strict $ rules sys
- return $ mkel "scc"
- $ toContents ( externalize vs u )
- ++ toContents p
- parseContents = wrap xread
-
-instance XRead Proof where
- xread = element "proof" $ do
- let cl = undefined
- rs <- foldr1 orelse
- [ element "trivial" $ return Trivial
- , element "reverse" $ fmap Reverse xread
- , element "as_trs" $ fmap As_TRS xread
- , element "manna_ness" $ do
- return () ; o <- xread ; p <- xread ; return $ MannaNess o p
- , element "mark_symbols" $ fmap MarkSymb xread
- , element "dp" $ fmap DP xread
- , complain "Proof"
- ]
- return $ Proof { claim = cl, reason = rs }
-
-externalize :: [ Identifier ]
- -> Rule ( Term Identifier Identifier )
- -> Rule ( Term Identifier ( Marked Identifier ) )
-externalize vs u =
- let -- HACK: rainbow/DPSCC requires variables be numbered
- -- according to inverse order in declaration (!?)
- m = Map.fromList
- $ zip ( reverse vs )
- $ map ( \ i -> mknullary $ "v" ++ show i ) [ 1 .. ]
- rename :: Identifier -> Identifier
- rename v = let Just w = Map.lookup v m in w
- handle ( Node f args ) = Node ( Hd_Mark $ unP f )
- $ map ( fmap Int_Mark . vmap rename ) args
- in Rule { lhs = handle $ lhs u, rhs = handle $ rhs u
- , relation = Strict , top = False }
-
--- | super ugly risky: name mangling
-unP :: Identifier -> Identifier
-unP k = let cs = show k
- in case last cs of 'P' -> mknullary $ init cs
-
-instance XmlContent Over_Graph where
- toContents og = return $ mkel ( map toLower $ show og ) []
-
-instance ( Typeable a, XmlContent a ) => XmlContent ( Marked a ) where
- toContents m = case m of
-{-
- Hd_Mark x -> return $ mkel "hd_mark" $ toContents x
- Int_Mark x -> return $ mkel "int_mark" $ toContents x
--}
--- HACK
- Hd_Mark x -> rmkel "sharp" $ rmkel "name" $ toContents x
- Int_Mark x -> rmkel "name" $ toContents x
-
- parseContents = wrap xread
-
-instance ( Typeable a, XmlContent a ) => XRead ( Marked a ) where
- xread = foldr1 orelse
- [ fmap Hd_Mark $ element "hd_mark" xread
- , fmap Int_Mark $ element "int_mark" xread
- , complain "Marked"
- ]
-
--- FIXME
-instance XRead Identifier where
- xread = CParser $ \ ( c : cs ) ->
- return ( mknullary "some_identifier" , cs )
- -- error $ info [c]
-
--- FIXME: we will need this for SCC
--- instance XmlContent TES where
-
diff --git a/TPDB/Xml.hs b/TPDB/Xml.hs
--- a/TPDB/Xml.hs
+++ b/TPDB/Xml.hs
@@ -13,6 +13,9 @@
mkel name cs = CElem ( Elem (N name) [] cs ) ()
rmkel name cs = return $ mkel name cs
+nospaceString :: String -> Content ()
+nospaceString s = CString False s ()
+
instance Typeable t => HTypeable t where
toHType x = let cs = show ( typeOf x ) in Prim cs cs
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,6 +1,6 @@
Name: tpdb
-Version: 0.8.4
-Author: Johannes Waldmann
+Version: 0.9.6
+Author: Alexander Bau, Johannes Waldmann
Maintainer: Johannes Waldmann
Category: Logic
License: GPL
@@ -28,19 +28,22 @@
-- test/3.15.xml, test/33.trs , test/z001.srs
Library
- Build-Depends: base==4.*, hxt, wl-pprint-text,
+ Build-Depends: base==4.*, hxt, wl-pprint-text, mtl,
parsec, time, containers, HaXml, filepath, hashable
Exposed-Modules:
TPDB.Data, TPDB.Data.Term, TPDB.Data.Xml
-- TPDB.Compress,
TPDB.Convert, TPDB.Input
- TPDB.Mirror, TPDB.DP
+ TPDB.Mirror
+ TPDB.DP, TPDB.DP.Graph, TPDB.DP.Transform, TPDB.DP.Unify, TPDB.DP.Usable, TPDB.DP.TCap,
TPDB.Pretty, TPDB.Plain.Write, TPDB.Plain.Read,
TPDB.XTC, TPDB.XTC.Read, TPDB.Xml,
TPDB.Xml.Pretty,
- TPDB.Rainbow.Proof.Xml, TPDB.Rainbow.Proof.Type
- TPDB.CPF.Proof.Xml, TPDB.CPF.Proof.Type
+ -- TPDB.Rainbow.Proof.Xml, TPDB.Rainbow.Proof.Type
+ TPDB.CPF.Proof.Write, TPDB.CPF.Proof.Read,
+ TPDB.CPF.Proof.Xml,
+ TPDB.CPF.Proof.Type, TPDB.CPF.Proof.Util
-- Executable Compressor
-- Main-is: Compressor.hs