horname 0.1.2.0 → 0.1.3.0

raw patch · 3 files changed

+55/−24 lines, 3 filesdep ~megaparsecPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: megaparsec

API changes (from Hackage documentation)

Files

• horname.cabal +1/−1
• src/Horname/Internal/SMT.hs +53/−22
• src/Horname/Internal/SMT/Parser.hs +1/−1

@@ -1,5 +1,5 @@ name:                horname-version:             0.1.2.0+version:             0.1.3.0 synopsis:            Rename function definitions returned by SMT solvers description:         Please see README.md homepage:            https://github.com/cocreature/horname#readme

@@ -1,6 +1,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-} module Horname.Internal.SMT where  import           Data.Data@@ -55,15 +56,15 @@     renameInBody m (List exprs) = List (map (renameInBody m) exprs)  insertBindings :: Map Text SExpr -> [SExpr] -> Map Text SExpr-insertBindings m bindings = foldl' insertBinding m bindings+insertBindings m bindings = foldl' (insertBinding m) m bindings -insertBinding :: Map Text SExpr -> SExpr -> Map Text SExpr-insertBinding m (List [StringLit key, val]) = Map.insert key val m-insertBinding _ _ = error "Syntax error in let bindings"+insertBinding :: Map Text SExpr -> Map Text SExpr -> SExpr -> Map Text SExpr+insertBinding oldMap m (List [StringLit key, val]) = Map.insert key (inlineLets' oldMap val) m+insertBinding _ _ _ = error "Syntax error in let bindings" --- | This is not correct in the presence of nested lets but these--- should never occur in the Z3 output and Eldarica doesn’t include--- any lets.+-- | This is not correct in the case of quantifiers but ignoring this+-- simplifies the implementation and seems to be enough for z3 and+-- eldarica inlineLets :: SExpr -> SExpr inlineLets = inlineLets' Map.empty @@ -87,7 +88,8 @@        (List [StringLit "-", e]) -> Right e        e -> Left e)     args-partitionPosNeg e = ([e],[])+partitionPosNeg (Neg e) = ([], [e])+partitionPosNeg e = ([e], [])  partition               :: (a -> Either b c) -> [a] -> ([b],[c]) partition p xs = foldr (select p) ([],[]) xs@@ -107,28 +109,60 @@ sumExprs [e] = e sumExprs args = List (StringLit "+" : args) +pattern And :: [SExpr] -> SExpr+pattern And args = List (StringLit "and" : args)++pattern Neg :: SExpr -> SExpr+pattern Neg arg = List [StringLit "-", arg]++pattern Or :: [SExpr] -> SExpr+pattern Or args = List (StringLit "or" : args)++pattern BinOp :: Text -> SExpr -> SExpr -> SExpr+pattern BinOp name op1 op2 = List [StringLit name, op1, op2]+ -- first pass of simplifications simplify :: SExpr -> SExpr -- (* (- 1) x) → x-simplify (List [StringLit "*", List [StringLit "-", IntLit i], expr]) =+simplify (BinOp "*" (Neg (IntLit i)) expr) =   let expr' =         if i == 1           then expr-          else List [StringLit "*", IntLit i, expr]-  in List [StringLit "-", expr']+          else BinOp "*" (IntLit i) expr+  in Neg expr' -- merge nested ands-simplify (List (StringLit "and":args)) =-  List (StringLit "and" : (andArgs ++ others))+simplify (And args) = And (andArgs ++ others)   where     (ands, others) =       partition         (\case-           List (StringLit "and":args') -> Left args'+           And args' -> Left args'            e -> Right e)         args     andArgs = concat ands+-- pull out common subexpressions of disjunctions+simplify (Or (arg:args)) =+  if null commonSubExprs+    then Or (arg : args)+    else And+           (commonSubExprs +++            [Or (map (removeSubExprs commonSubExprs) (arg : args))])+  where+    commonSubExprs =+      filter+        (\arg' -> all (arg' `subsumedBy`) args)+        (case arg of+           And exprs -> exprs+           _ -> [])+    subsumedBy :: SExpr -> SExpr -> Bool+    subsumedBy e (And args') = e `elem` args'+    subsumedBy _ _ = False+    removeSubExprs :: [SExpr] -> SExpr -> SExpr+    removeSubExprs subExprs (And exprs) =+      And (filter (\e -> not (e `elem` subExprs)) exprs)+    removeSubExprs _ e = e -- Move negative and positive arguments to the same side of a comparison-simplify (List [StringLit opName, arg1, arg2])+simplify (BinOp opName arg1 arg2)   | opName `elem` comparisonOps =     case (partitionPosNeg arg1, partitionPosNeg arg2) of       ((posLeft, negLeft), (posRight, negRight)) ->@@ -142,12 +176,10 @@   List (StringLit "+" : (sepSubtraction =<< args))   where     sepSubtraction :: SExpr -> [SExpr]-    sepSubtraction (List [StringLit "-", arg1, arg2]) =-      [arg1, List [StringLit "-", arg2]]+    sepSubtraction (BinOp "-" arg1 arg2) = [arg1, Neg 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 (List [StringLit "not", Or args]) = And (map negateExpr args) simplify e = e  antiSymmetricOp :: Text -> Bool@@ -155,8 +187,7 @@ -- second pass of simplifications simplify' :: SExpr -> SExpr -- transform two inequalities to an equality-simplify' (List (StringLit "and":args)) =-  List (StringLit "and" : other ++ mergeInequalities inequality)+simplify' (And args) = And (other ++ mergeInequalities inequality)   where     (inequality, other) =       List.partition@@ -169,7 +200,7 @@     mergeInequalities (e@(List [StringLit op, expr1, expr2]):rest) =       let reversedE = List [StringLit op, expr2, expr1]       in if reversedE `elem` rest-           then List [StringLit "=", expr1, expr2] :+           then BinOp "=" expr1 expr2 :                 mergeInequalities (filter (not . (`elem` [e, reversedE])) rest)            else e : mergeInequalities rest     mergeInequalities (e:es) = e : mergeInequalities es

@@ -62,7 +62,7 @@         digits <- many digitChar         pure (IntLit (read (alphaNum : digits)))       | otherwise -> do-        rest <- many (noneOf [' ', ')'])+        rest <- many (noneOf [' ', '\t', '\n', ')'])         pure . StringLit . Text.pack $ alphaNum : rest  parseDefineFun :: Parser DefineFun