packages feed

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 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