tpdb 0.8.4 → 0.9.6
raw patch · 20 files changed
+807/−711 lines, 20 filesdep +mtl
Dependencies added: mtl
Files
- TPDB/CPF/Proof/Read.hs +85/−0
- TPDB/CPF/Proof/Type.hs +70/−12
- TPDB/CPF/Proof/Util.hs +26/−0
- TPDB/CPF/Proof/Write.hs +323/−0
- TPDB/CPF/Proof/Xml.hs +6/−172
- TPDB/DP.hs +4/−49
- TPDB/DP/Graph.hs +53/−0
- TPDB/DP/TCap.hs +29/−0
- TPDB/DP/Transform.hs +71/−0
- TPDB/DP/Unify.hs +38/−0
- TPDB/DP/Usable.hs +43/−0
- TPDB/Data.hs +10/−0
- TPDB/Data/Term.hs +12/−0
- TPDB/Data/Xml.hs +16/−1
- TPDB/Input.hs +5/−5
- TPDB/Pretty.hs +4/−0
- TPDB/Rainbow/Proof/Type.hs +0/−176
- TPDB/Rainbow/Proof/Xml.hs +0/−290
- TPDB/Xml.hs +3/−0
- tpdb.cabal +9/−6
+ TPDB/CPF/Proof/Read.hs view
@@ -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)+
TPDB/CPF/Proof/Type.hs view
@@ -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
+ TPDB/CPF/Proof/Util.hs view
@@ -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"
+ TPDB/CPF/Proof/Write.hs view
@@ -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+ ]
TPDB/CPF/Proof/Xml.hs view
@@ -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
TPDB/DP.hs view
@@ -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 }
+ TPDB/DP/Graph.hs view
@@ -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)))"+
+ TPDB/DP/TCap.hs view
@@ -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 +
+ TPDB/DP/Transform.hs view
@@ -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 + }
+ TPDB/DP/Unify.hs view
@@ -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+
+ TPDB/DP/Usable.hs view
@@ -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 -> []+
TPDB/Data.hs view
@@ -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 )
TPDB/Data/Term.hs view
@@ -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
TPDB/Data/Xml.hs view
@@ -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 "<var>foo</var>"+-- a constructor symbol is also an Identifier+-- but it must look like "<funapp><name>bar<name>..."+-- so it should be wrapped into <name>+-- but no, if the constructor is sharped (or labelled)+-- then it must look like "<funapp><sharp><name>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 ) () ] ->
TPDB/Input.hs view
@@ -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
TPDB/Pretty.hs view
@@ -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)
− TPDB/Rainbow/Proof/Type.hs
@@ -1,176 +0,0 @@-{-# language OverloadedStrings #-}-{-# language ExistentialQuantification #-}-{-# language DeriveDataTypeable #-}---- | internal representation of Rainbow termination proofs,--- see <http://color.loria.fr/>--- 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--}-
− TPDB/Rainbow/Proof/Xml.hs
@@ -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 <integer value="42"/>--- 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-
TPDB/Xml.hs view
@@ -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
tpdb.cabal view
@@ -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