tpdb 0.3 → 0.6.0
raw patch · 16 files changed
+516/−37 lines, 16 filesdep +directorydep +filepathnew-component:exe:Compressor
Dependencies added: directory, filepath
Files
- Compressor.hs +80/−0
- TPDB/CPF/Proof/Type.hs +18/−10
- TPDB/CPF/Proof/Xml.hs +41/−4
- TPDB/Compress.hs +179/−0
- TPDB/Convert.hs +36/−0
- TPDB/Data.hs +18/−4
- TPDB/Data/Xml.hs +7/−1
- TPDB/Input.hs +48/−0
- TPDB/Mirror.hs +19/−0
- TPDB/Plain/Read.hs +6/−3
- TPDB/Plain/Write.hs +12/−3
- TPDB/Pretty.hs +11/−0
- TPDB/Rainbow/Proof/Type.hs +21/−3
- TPDB/Rainbow/Proof/Xml.hs +9/−4
- TPDB/XTC/Read.hs +3/−3
- tpdb.cabal +8/−2
+ Compressor.hs view
@@ -0,0 +1,80 @@+{-# language DoAndIfThenElse #-}++import TPDB.Compress (compress)+import TPDB.DP ( dp, Marked (Auxiliary) )+import TPDB.Data+import TPDB.XTC.Read ( readProblems )+import TPDB.Plain.Write ( )+import TPDB.Pretty ( pretty )+import Text.PrettyPrint.HughesPJ + ( text, ($$), nest, vcat )++import System.Environment+import System.IO+import System.Directory+import Control.Monad ( guard, forM )+import Data.List ( isSuffixOf, isPrefixOf )+import qualified Data.Set as S++-- | give file/dir name(s) on cmd line.+-- recursively collect all *.xml files,+-- and apply TRS compression.++main = do+ hSetBuffering stdout LineBuffering + args <- getArgs+ ss <- collect args+ putStrLn "action"+ forM ( map dp ss ) $ \ s -> do+ print $ text "original TRS" </> pretty s + let ( com, rules ) = compress supply s+ print $ text "compressed TRS" </> vcat+ ( pretty com : map pretty rules )+ print $ judge s++p </> q = p $$ nest 4 q++judge sys = + let csys = compress supply sys+ in ( cost_trs sys , cost_comp csys )++supply = do + i <- [ 0 .. ] + return $ Auxiliary $ mknullary $ "c" ++ show i++cost_comp ( s, sub ) = + cost_trs s + cost_sub sub+ +cost_sub sub = sum $ do+ ((f, af), Just (g, k, h, ca)) <- sub+ return ca++cost_trs s = sum $ do+ u <- rules s+ t <- [ lhs u, rhs u ]+ return $ cost_term t++cost_term t = sum $ do + (p,s) <- positions t + return $ multiplications s++multiplications t = case t of+ Node f xs -> sum $ do+ x @ Node {} <- xs+ return $ S.size $ vars x+ _ -> 0 ++collect fs = do+ let special d = isPrefixOf "." d+ fss <- forM fs $ \ f -> do+ d <- doesDirectoryExist f+ if d + then do+ fs <- getDirectoryContents f+ collect $ map ( ( f ++ "/" ) ++ )+ $ filter (not . special) fs+ else if isSuffixOf ".xml" f+ then fmap (map trs) $ readProblems f+ else return []+ return $ concat fss+
TPDB/CPF/Proof/Type.hs view
@@ -19,9 +19,17 @@ data CertificationProblem = CertificationProblem { input :: CertificationProblemInput - , proof :: Proof } + , cpfVersion :: String -- urgh+ , proof :: Proof + , origin :: Origin + } deriving ( Typeable ) +data Origin = ProofOrigin Tool + deriving Typeable+data Tool = Tool { name :: String , version :: String } + deriving Typeable+ data CertificationProblemInput = TrsInput { trsinput_trs :: TRS Identifier Identifier } -- ^ this is actually not true, since instead of copying from XTC,@@ -42,12 +50,10 @@ data TrsTerminationProof = RIsEmpty-{-- | RuleRemoval { orderingConstraintProof :: OrderingConstraintProof+ | RuleRemoval { rr_orderingConstraintProof :: OrderingConstraintProof , trs :: TRS Identifier Identifier , trsTerminationProof :: TrsTerminationProof } --} | DpTrans { dptrans_dps :: DPS , markedSymbols :: Bool , dptrans_dpProof :: DpProof } | StringReversal { trs :: TRS Identifier Identifier@@ -56,7 +62,7 @@ deriving ( Typeable ) data DpProof = PIsEmpty - | RedPairProc { orderingConstraintProof :: OrderingConstraintProof+ | RedPairProc { dp_orderingConstraintProof :: OrderingConstraintProof , red_pair_dps :: DPS , redpairproc_dpProof :: DpProof } deriving ( Typeable ) @@ -77,6 +83,9 @@ deriving ( Typeable ) data Domain = Naturals + | Rationals Rational+ | Arctic Domain+ | Tropical Domain deriving ( Typeable ) data Interpret = forall s . XmlContent s => Interpret @@ -89,6 +98,7 @@ data Polynomial = Sum [ Polynomial ] | Product [ Polynomial ] | Polynomial_Coefficient Coefficient+ | Polynomial_Variable String deriving ( Typeable ) data Coefficient = Vector [ Coefficient ]@@ -96,10 +106,8 @@ | forall a . XmlContent a => Coefficient_Coefficient a deriving ( Typeable ) -----+data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite+ deriving Typeable +class ToExotic a where toExotic :: a -> Exotic
TPDB/CPF/Proof/Xml.hs view
@@ -25,6 +25,7 @@ import qualified Data.Time as T import Control.Monad import Data.Typeable+import Data.Ratio tox :: CertificationProblem -> Document () tox p = @@ -36,9 +37,21 @@ 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 )@@ -65,7 +78,8 @@ Sharp q -> rmkel "sharp" $ toContents q instance XmlContent DPS where- toContents ( DPS rules ) = rmkel "dps" $ concat $ map toContents rules+ toContents ( DPS rules ) = rmkel "dps" + $ rmkel "rules" $ rules >>= toContents instance XmlContent TrsTerminationProof where toContents p = rmkel "trsTerminationProof" $ case p of@@ -73,12 +87,19 @@ 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 ( orderingConstraintProof p )+ $ toContents ( dp_orderingConstraintProof p ) ++ toContents ( red_pair_dps p ) ++ toContents ( redpairproc_dpProof p ) @@ -102,11 +123,21 @@ 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 } -> - toContents s+ sharp_name_HACK ( toContents s ) ++ rmkel "arity" [ CString False ( show ( arity i )) () ] ++ toContents ( value i ) @@ -119,7 +150,9 @@ 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 )@@ -127,7 +160,11 @@ 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" []
+ TPDB/Compress.hs view
@@ -0,0 +1,179 @@+{-# language TemplateHaskell #-}++module TPDB.Compress where++import TPDB.Data hiding ( trs, arity )+import TPDB.Plain.Write ()+import qualified TPDB.Plain.Read (trs) -- for testing+import TPDB.Pretty ++import Control.Monad ( guard ) +import qualified Data.Set as S+import qualified Data.Map.Strict as M+import Data.List ( sortBy )+import Data.Ord ( comparing )+++-- | compute a compressed version of the TRS.+-- Warning: in the output, the arities of fresh identifiers will be nonsensical+compress :: ( Ord s )+ => [s] -- ^ supply of function symbols. This can be any infinite list,+ -- the implementation will filter out those elements that+ -- occur in the original TRS's signature.+ -> TRS v s + -> ( TRS v s + , [ ((s, Int), Maybe (s,Int,s,Int) ) ] + ) -- ^ ((f, a), Just (g,i,h,a)) semantics: new function symbols f+ -- by substituting h in the i-th position (start at 0) of g.+ -- arity of child is a+ -- ((f, a), Nothing ) semantics: f of arity a is an "old" function symbol.+ -- output is in dependency order (will only refer to previously defined symbols).+compress pool sys = + let osig = ohsig sys+ forbidden = M.keysSet osig+ fresh = filter ( `S.notMember` forbidden ) pool+ con = make fresh sys+ in ( trs con + , map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig )+ ++ map ( \ (f, p) -> ( (f, arity p), Just (parent p, branch p, child p, child_arity p) ) ) + ( reverse $ defs con )+ )++ohsig sys = M.fromListWith ( \ o n -> if o == n then o else error "different arities" ) + $ do u <- rules sys ; t <- [ lhs u , rhs u ]+ ( _ , Node f args ) <- positions t+ return ( f, length args )++dont_compress pool sys = + let osig = ohsig sys+ in ( sys , map ( \ fa -> ( fa, Nothing ) ) ( M.toList osig ) )+ ++data Pattern s = Pattern+ { parent :: ! s+ , branch :: ! Int+ , child :: ! s+ , arity :: ! Int+ , child_arity :: ! Int+ , has_grand_child :: ! Bool + }+ deriving ( Eq, Ord )++data Container v s = Container + { trs :: TRS v s+ , defs :: [( s, Pattern s)] + }++make fresh trs = handle fresh $ Container trs []+++handle free con = + case -- take 1 $ + disjoint $ best_patterns $ trs con of+ [] -> con+ ps -> + let ( pre, post ) + = splitAt ( length ps ) free+ here = zip pre ps + in handle post+ $ con { trs = apply_system here $ trs con+ , defs = here ++ defs con+ }++patterns_in_term t = + nonoverlapping t ++ overlapping t++overlapping t = do+ (pos, Node f xs) <- positions t+ ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs+ guard $ f == g+ let sub = case ys !! k of + Node h _ -> True+ _ -> False+ guard $ if sub then even $ length pos else True + let r = not $ null $ do Node {} <- ys ; return ()+ return $ Pattern { arity = length xs - 1 + length ys+ , parent = f, branch = k+ , child = g, child_arity = length ys+ , has_grand_child = r + }++nonoverlapping t = do+ Node f xs <- subterms t+ ( k , x @ ( Node g ys ) ) <- zip [ 0 .. ] xs+ guard $ f /= g+ let r = not $ null $ do Node {} <- ys ; return ()+ return $ Pattern { arity = length xs - 1 + length ys+ , parent = f, branch = k+ , child = g, child_arity = length ys+ , has_grand_child = r + }++patterns_in_rule u = do+ t <- [ lhs u, rhs u ]+ patterns_in_term t++patterns trs = do+ u <- rules trs+ patterns_in_rule u++disjoint ps =+ let h seen [] = []+ h seen (p:ps) = + if S.notMember (parent p) seen+ && S.notMember (child p) seen+ then p : h (S.insert (parent p) + $ S.insert (child p) seen) ps+ else h seen ps + in h S.empty ps ++best_patterns trs = do+ let pns = sortBy ( comparing ( negate . snd ))+ $ M.toList $ collect $ patterns trs+ let threshold = case pns of + [] -> 0+ (p,n) : _ -> div n 2+ (p,n) <- takeWhile ( \ (p,n) -> n >= threshold ) pns+ guard $ ( n > 1 ) || ( n == 1 && has_grand_child p )+ return p+++apply_system fgps trs = do+ trs { rules = map ( apply_rule fgps ) $ rules trs }++apply_rule fgps u = + u { lhs = apply_term fgps $ lhs u+ , rhs = apply_term fgps $ rhs u+ }++apply_term _ ( Var v ) = Var v+apply_term fgps t @ (Node top args) = + let Node newtop newargs = multi_matches fgps t+ in Node newtop $ map (apply_term fgps) newargs+ +multi_matches [] t = t+multi_matches ((fg, p@Pattern{parent=f,branch=i,child=g}) : fgps ) t@(Node top args) = + if matches p t+ then let ( pre, Node _ sub : post) = splitAt i args + in Node fg ( pre ++ sub ++ post ) + else multi_matches fgps t ++matches ( Pattern { parent = f, branch = i, child = g } ) + ( Node top args ) | top == f = + case args !! i of+ Node bot _ | bot == g -> True+ _ -> False+matches p _ = False++++collect xs = M.fromListWith (+) $ do + x <- xs + return ( x, child_arity x )+++invert :: ( Ord a, Ord b )+ => M.Map a b -> M.Map b [a]+invert fm = M.fromListWith (++) $ do+ ( k, v ) <- M.toList fm+ return ( v, [k] )
+ TPDB/Convert.hs view
@@ -0,0 +1,36 @@+module TPDB.Convert where++import TPDB.Data+import Control.Monad ( forM, guard )++srs2trs :: SRS s -> TRS Identifier s+srs2trs s = s { separate = False+ , rules = map convert_srs_rule $ rules s+ } ++convert_srs_rule u = + let v = Identifier "x" 0 + in u { lhs = unspine v $ lhs u+ , rhs = unspine v $ rhs u + } + +trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )+trs2srs t = do+ us <- forM ( rules t ) convert_trs_rule + return $ t { separate = True , rules = us }++convert_trs_rule u = do+ ( left_spine, left_base ) <- spine $ lhs u+ ( right_spine, right_base ) <- spine $ rhs u+ guard $ left_base == right_base + return $ u { lhs = left_spine, rhs = right_spine }++unspine :: v -> [s] -> Term v s+unspine v = foldr ( \ c t -> Node c [ t ] ) ( Var v )++spine :: Term v s -> Maybe ( [s], v )+spine t = case t of+ Node f [ a ] -> do+ ( sp, base ) <- spine a + return ( f : sp, base )+ Var v -> return ( [] , v )
TPDB/Data.hs view
@@ -25,12 +25,24 @@ --------------------------------------------------------------------- +data Relation = Strict | Weak | Equal deriving ( Eq, Ord, Typeable, Show )+ data Rule a = Rule { lhs :: a, rhs :: a - , strict :: Bool+ , relation :: Relation , top :: Bool } deriving ( Eq, Ord, Typeable ) +strict :: Rule a -> Bool+strict u = case relation u of Strict -> True ; _ -> False++weak :: Rule a -> Bool+weak u = case relation u of Weak -> True ; _ -> False++equal :: Rule a -> Bool+equal u = case relation u of Equal -> True ; _ -> False++ data RS s r = RS { signature :: [ s ] -- ^ better keep order in signature (?) , rules :: [ Rule r ]@@ -40,8 +52,10 @@ strict_rules sys = do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )-non_strict_rules sys = - do u <- rules sys ; guard $ not $ strict u ; return ( lhs u, rhs u )+weak_rules sys = + do u <- rules sys ; guard $ weak u ; return ( lhs u, rhs u )+equal_rules sys = + do u <- rules sys ; guard $ equal u ; return ( lhs u, rhs u ) type TRS v s = RS s ( Term v s ) @@ -79,7 +93,7 @@ from_strict_rules :: Bool -> [(t,t)] -> RS i t from_strict_rules sep rs = RS { rules = map ( \ (l,r) ->- Rule { strict = True, top = False, lhs = l, rhs = r } ) rs+ Rule { relation = Strict, top = False, lhs = l, rhs = r } ) rs , separate = sep }
TPDB/Data/Xml.hs view
@@ -38,8 +38,14 @@ -} -- for CPF: toContents ( Node f args ) = rmkel "funapp" - $ rmkel "name" ( toContents f )+ $ sharp_name_HACK ( toContents f ) ++ map ( \ arg -> mkel "arg" $ toContents arg ) args+++sharp_name_HACK e = case e of+ [ CElem ( Elem (N "sharp") [] cs ) () ] -> + rmkel "sharp" $ rmkel "name" cs+ _ -> rmkel "name" e
+ TPDB/Input.hs view
@@ -0,0 +1,48 @@+module TPDB.Input where++import TPDB.Data+import TPDB.Plain.Read+import TPDB.XTC.Read+import TPDB.Convert++import System.FilePath.Posix ( splitExtension )++-- | read input from file with given name.+-- can have extension .srs, .trs, .xml.++get :: FilePath + -> IO ( Either (TRS Identifier Identifier) + ( SRS Identifier ) )+get f = do+ let ( base, ext ) = splitExtension f + case ext of + ".srs" -> do+ s <- readFile f + case srs s of+ Left err -> error err+ Right t -> return $ Right t+ ".trs" -> do + s <- readFile f+ case TPDB.Plain.Read.trs s of+ Left err -> error err+ Right t -> return $ Left t + ".xml" -> do+ ps <- readProblems f+ case ps of + [ p ] -> return $ Left $ TPDB.Data.trs p++get_trs f = do+ x <- get f+ return $ case x of+ Right x -> srs2trs x+ Left x -> x++get_srs f = do+ x <- get f+ return $ case x of+ Right x -> x+ Left x -> case trs2srs x of+ Nothing -> error "not an SRS"+ Just x -> x+ +
+ TPDB/Mirror.hs view
@@ -0,0 +1,19 @@+module TPDB.Mirror where++import TPDB.Data+import TPDB.Convert++import Control.Monad ( forM, guard )++-- | if input is SRS, reverse lhs and rhs of each rule+mirror :: TRS Identifier s + -> Maybe ( TRS Identifier s )+mirror trs = do+ us <- forM (rules trs) $ \ u -> do+ ( left_spine, left_base ) <- spine $ lhs u+ ( right_spine, right_base ) <- spine $ rhs u+ guard $ left_base == right_base + return $ u { lhs = unspine left_base $ reverse left_spine+ , rhs = unspine right_base $ reverse right_spine+ }+ return $ trs { rules = us }
TPDB/Plain/Read.hs view
@@ -58,10 +58,13 @@ instance Reader u => Reader ( Rule u ) where reader = do l <- reader- s <- do reservedOp lexer "->" ; return True- <|> do reservedOp lexer "->=" ; return False+ rel <- do reservedOp lexer "->" ; return Strict+ <|> do reservedOp lexer "->=" ; return Weak+ -- FIXME: for the moment, we do not parse this+ -- as it would deviate from published TPDB syntax+ -- <|> do reservedOp lexer "=" ; return Equal r <- reader- return $ Rule { lhs = l, strict = s, top = False, rhs = r }+ return $ Rule { lhs = l, relation = rel, top = False, rhs = r } data Declaration u = Var_Declaration [ Identifier ]
TPDB/Plain/Write.hs view
@@ -9,6 +9,8 @@ import TPDB.Pretty import Text.PrettyPrint.HughesPJ +import Data.List ( nub )+ instance Pretty Identifier where pretty i = text $ name i @@ -21,14 +23,18 @@ instance PrettyTerm a => Pretty ( Rule a ) where pretty u = hsep [ prettyTerm $ lhs u- , if strict u then text "->" else text "->="+ , case relation u of + Strict -> text "->" + Weak -> text "->="+ Equal -> text "=" -- FIXME: implement "top" annotation , prettyTerm $ rhs u ] -class PrettyTerm a where prettyTerm :: a -> Doc+class PrettyTerm a where + prettyTerm :: a -> Doc -instance Pretty s => PrettyTerm [s] where+instance Pretty s => PrettyTerm [s] where prettyTerm xs = hsep $ map pretty xs instance ( Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where@@ -40,6 +46,9 @@ vcat ( ( if separate sys then punctuate comma else id ) $ map pretty $ rules sys )+ -- FIXME: variables are not shown (and it is impossible to compute+ -- them here, this is actually a TPDB format design error, + -- since variables should be local (per rule), not global) -- FIXME: output strategy, theory ]
TPDB/Pretty.hs view
@@ -9,5 +9,16 @@ instance ( Pretty a, Pretty b ) => Pretty (a,b) where pretty (x,y) = parens $ fsep $ punctuate comma [ pretty x, pretty y ] +instance ( Pretty a, Pretty b, Pretty c ) => Pretty (a,b,c) where+ pretty (x,y,z) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z ]++instance ( Pretty a, Pretty b, Pretty c, Pretty d ) => Pretty (a,b,c,d) where+ pretty (x,y,z,u) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z, pretty u ]+ instance Pretty a => Pretty [a] where pretty xs = brackets $ fsep $ punctuate comma $ map pretty xs++instance Pretty a => Pretty (Maybe a) where+ pretty m = case m of+ Nothing -> text "Nothing"+ Just x -> text "Just" <+> pretty x -- FIXME: parens missing
TPDB/Rainbow/Proof/Type.hs view
@@ -13,6 +13,8 @@ import TPDB.Plain.Write () -- just instances import Text.PrettyPrint.HughesPJ +import qualified TPDB.CPF.Proof.Type as C+ import Text.XML.HaXml.XmlContent.Haskell hiding ( text ) import qualified Text.Parsec as P @@ -25,9 +27,12 @@ data Matrix a = Matrix [ Vector a ] deriving Typeable -data MaxPlus = MinusInfinite | Finite Integer+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 ]@@ -43,7 +48,7 @@ type Polynomial_Int = Interpretation Poly_Fun data Interpretation f = forall k a - . ( XmlContent k, XmlContent a, Typeable a ) -- Haskell2Xml a + . ( XmlContent k, XmlContent a, C.ToExotic a, Typeable a ) -- Haskell2Xml a => Interpretation { mi_domain :: Domain , mi_dim :: Integer@@ -153,6 +158,19 @@ -+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 view
@@ -6,6 +6,8 @@ import TPDB.Rainbow.Proof.Type +import qualified TPDB.CPF.Proof.Type as C+ import TPDB.Xml import TPDB.Data.Xml -- import Matrix.MaxPlus ( MaxPlus )@@ -113,7 +115,8 @@ 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 -------------------------------------------------------------------------------- @@ -151,7 +154,7 @@ -- | FIXME this is broken because the keys could be -- Identifier or Marked Identifier-mai :: forall a . ( Typeable a, XmlContent a )+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@@ -225,7 +228,8 @@ [ 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 "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"@@ -245,7 +249,8 @@ 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, strict = True , top = False } + in Rule { lhs = handle $ lhs u, rhs = handle $ rhs u+ , relation = Strict , top = False } -- | super ugly risky: name mangling unP :: Identifier -> Identifier
TPDB/XTC/Read.hs view
@@ -73,8 +73,8 @@ getTRS = proc x -> do sig <- getSignature <<< getChild "signature" -< x- str <- getRules True <<< getChild "rules" -< x- nostr <- listA ( getRules False <<< getChild "relrules" <<< getChild "rules" ) -< x+ str <- getRules Strict <<< getChild "rules" -< x+ nostr <- listA ( getRules Weak <<< getChild "relrules" <<< getChild "rules" ) -< x -- FIXME: check that symbols are use with correct arity th <- listA ( atTag "theory" ) -< x returnA -< case th of@@ -98,7 +98,7 @@ getRule str = proc x -> do l <- getTerm <<< isElem <<< gotoChild "lhs" -< x r <- getTerm <<< isElem <<< gotoChild "rhs" -< x- returnA -< Rule { lhs = l, strict = str, rhs = r, top = False }+ returnA -< Rule { lhs = l, relation = str, rhs = r, top = False } readProblems :: FilePath -> IO [ Problem Identifier Identifier ] readProblems file = do
tpdb.cabal view
@@ -1,5 +1,5 @@ Name: tpdb-Version: 0.3+Version: 0.6.0 Author: Johannes Waldmann Maintainer: Johannes Waldmann Category: Science@@ -26,14 +26,20 @@ -- test/3.15.xml, test/33.trs , test/z001.srs Library- Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml+ Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml, filepath Exposed-Modules: TPDB.Data, TPDB.Data.Term, TPDB.Data.Xml+ TPDB.Compress, TPDB.Convert, TPDB.Input+ TPDB.Mirror, TPDB.Pretty, TPDB.Plain.Write, TPDB.Plain.Read, TPDB.XTC, TPDB.XTC.Read, TPDB.Xml, TPDB.Rainbow.Proof.Xml, TPDB.Rainbow.Proof.Type TPDB.CPF.Proof.Xml, TPDB.CPF.Proof.Type++Executable Compressor+ Main-is: Compressor.hs+ Build-depends: base==4.*, containers, directory, pretty, hxt, parsec Test-Suite XML Build-Depends: base==4.*, hxt, pretty, parsec, time, containers, HaXml