horname 0.1.0.0 → 0.1.1.0
raw patch · 3 files changed
+26/−4 lines, 3 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Horname.Internal.SMT: negateExpr :: SExpr -> SExpr
Files
- horname.cabal +1/−1
- src/Horname/Internal/SMT.hs +13/−2
- src/Horname/Internal/SMT/Parser.hs +12/−1
horname.cabal view
@@ -1,5 +1,5 @@ name: horname-version: 0.1.0.0+version: 0.1.1.0 synopsis: Rename function definitions returned by SMT solvers description: Please see README.md homepage: https://github.com/cocreature/horname#readme
src/Horname/Internal/SMT.hs view
@@ -108,8 +108,12 @@ simplify :: SExpr -> SExpr -- (* (- 1) x) → x-simplify (List [StringLit "*", List [StringLit "-", IntLit 1], expr]) =- List [StringLit "-", expr]+simplify (List [StringLit "*", List [StringLit "-", IntLit i], expr]) =+ let expr' =+ if i == 1+ then expr+ else List [StringLit "*", IntLit i, expr]+ in List [StringLit "-", expr'] -- merge nested ands simplify (List (StringLit "and":args)) = List (StringLit "and" : (andArgs ++ others))@@ -139,7 +143,14 @@ sepSubtraction (List [StringLit "-", arg1, arg2]) = [arg1, List [StringLit "-", arg2]] sepSubtraction e = [e]+-- transform (not (or (not …))) to (and …)+simplify (List [StringLit "not", List (StringLit "or":args)]) =+ List (StringLit "and" : map negateExpr args) simplify e = e++negateExpr :: SExpr -> SExpr+negateExpr (List [StringLit "not", expr]) = expr+negateExpr expr = List [StringLit "not", expr] extractDefinitions :: Map Text [Text] -> [DefineFun] -> [DefineFun] extractDefinitions decls defs =
src/Horname/Internal/SMT/Parser.hs view
@@ -5,6 +5,7 @@ import Data.Generics.Uniplate.Data import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map+import Data.Monoid import Data.Text (Text) import qualified Data.Text as Text import Horname.Internal.SMT@@ -15,7 +16,17 @@ parseName = Text.pack <$> some (noneOf [' ', '\n', ')']) parseSort :: Parser Sort-parseSort = Sort . Text.pack <$> some (noneOf [' ', '\n', ')'])+parseSort = do+ c <- noneOf [' ', '\n', ')']+ case c of+ '(' -> do+ space+ args <- map (\(Sort t) -> t) <$> sepBy parseSort someSpace+ _ <- char ')'+ pure $ Sort ("(" <> Text.intercalate " " args <> ")")+ c' -> do+ rest <- many (noneOf [' ', '\n', ')'])+ pure (Sort (Text.pack (c' : rest))) parseArg :: Parser Arg parseArg = do