term-rewriting 0.3.0.1 → 0.4

raw patch · 5 files changed

+25/−8 lines, 5 files

Files

• LICENSE +1/−1
• src/Data/Rewriting/Problem/Parse.hs +11/−0
• src/Data/Rewriting/Problem/Pretty.hs +10/−6
• src/Data/Rewriting/Problem/Type.hs +2/−0
• term-rewriting.cabal +1/−1

@@ -1,6 +1,6 @@ term-rewriting library -- basic first order term rewriting. -Copyright (c) 2011-2017 by Martin Avanzini, Bertram Felgenhauer and+Copyright (c) 2011-2019 by Martin Avanzini, Bertram Felgenhauer and Christian Sternagel.  Permission is hereby granted, free of charge, to any person obtaining a

@@ -71,6 +71,7 @@                                                                          Prob.weakRules = [] } ,                                       Prob.variables  = [] ,                                       Prob.symbols    = [] ,+                                      Prob.signature  = Nothing,                                       Prob.comment    = Nothing }  @@ -89,10 +90,12 @@   parseDecls = many1 parseDecl   parseDecl =  decl "VAR"       vars       (\ e p -> p {Prob.variables = e `union` Prob.variables p})            <|> decl "THEORY"    theory     (\ e p -> p {Prob.theory = maybeAppend Prob.theory e p})+           <|> decl "SIG"       signature  (\ e p -> p {Prob.signature = maybeAppend Prob.signature e p})            <|> decl "RULES"     rules      (\ e p -> p {Prob.rules   = e, --FIXME multiple RULES blocks?                                                         Prob.symbols = Rules.funsDL (Prob.allRules e) [] })            <|> decl "STRATEGY"  strategy   (\ e p -> p {Prob.strategy = e})            <|> decl "STARTTERM" startterms (\ e p -> p {Prob.startTerms = e})+           <|> (decl "COMMENT"   comment   (\ e p -> p {Prob.comment = maybeAppend Prob.comment e p}) <?> "comment")            <|> (par comment >>= modifyProblem . (\ e p -> p {Prob.comment = maybeAppend Prob.comment e p}) <?> "comment")   decl name p f = try (par $ do       lex $ string name@@ -103,6 +106,14 @@ vars :: (Stream s (Either ProblemParseError) Char) => WSTParser s [String] vars = do vs <- many (lex $ ident "()," [])           return vs++signature :: (Stream s (Either ProblemParseError) Char) => WSTParser s [(String,Int)]+signature = many fundecl+    where+        fundecl = par (do+            f  <- lex $ ident "()," []+            ar <- lex (read <$> many1 digit)+            return $ (f,ar))  theory :: (Stream s (Either ProblemParseError) Char) => WSTParser s [Prob.Theory String String] theory = many thdecl where

@@ -26,13 +26,14 @@ prettyWST :: (f -> Doc) -> (v -> Doc) -> Problem f v -> Doc prettyWST fun var prob =     printWhen (sterms /= AllTerms) (block "STARTTERM" $ text "CONSTRUCTOR-BASED")-    <$$> printWhen (strat /= Full) (block "STRATEGY" $ ppStrat strat)-    <$$> maybeblock "THEORY" theory ppTheories-    <$$> block "VAR" (ppVars $ variables prob)-    <$$> block "RULES" (ppRules $ rules prob)-    <$$> maybeblock "COMMENT" comment text+    <> printWhen (strat /= Full) (block "STRATEGY" $ ppStrat strat)+    <> maybeblock "THEORY" theory ppTheories+    <> block "VAR" (ppVars $ variables prob)+    <> maybeblock "SIG" signature ppSignature+    <> block "RULES" (ppRules $ rules prob)+    <> maybeblock "COMMENT" comment text -  where block n pp = parens $ hang 3 $ text n <$$> pp+  where block n pp = (parens $ (hang 3 $ text n <$$> pp) <> linebreak) <> linebreak         maybeblock n f fpp = case f prob of                                Just e -> block n (fpp e)                                Nothing -> empty@@ -45,6 +46,9 @@         ppTheories thys = align $ vcat [ppThy thy | thy <- thys]             where ppThy (SymbolProperty p fs) = block p (align $ fillSep [ fun f | f <- fs ])                   ppThy (Equations rs)        = block "EQUATIONS" $ vcat [ppRule "==" r | r <- rs]++        ppSignature sigs = align $ fillSep [ppSig sig | sig <- sigs]+            where ppSig (f,i) = parens $ fun f <+> int i          ppRules rp = align $ vcat ([ppRule "->" r | r <- strictRules rp]                                    ++ [ppRule "->=" r | r <- weakRules rp])

@@ -39,6 +39,7 @@                            , rules      :: RulesPair f v                            , variables  :: [v]                            , symbols    :: [f]+                           , signature  :: Maybe [(f, Int)]                            , comment    :: Maybe String} deriving (Show)  allRules :: RulesPair f v -> [Rule f v]@@ -52,6 +53,7 @@            , rules = mapRulesPair ffun fvar (rules prob)            , variables = P.map fvar (variables prob)            , symbols = P.map ffun (symbols prob)+           , signature = fmap (P.map (\(f, a) -> (ffun f, a))) (signature prob)            , comment = comment prob}                mapTheory :: (f -> f') -> (v -> v') -> Theory f v -> Theory f' v'

@@ -1,5 +1,5 @@ name:          term-rewriting-version:       0.3.0.1+version:       0.4 stability:     experimental author:        Martin Avanzini,                Bertram Felgenhauer,