expressions-z3 0.1.3 → 0.1.4

raw patch · 3 files changed

+9/−4 lines, 3 filesdep +list-tdep ~z3

Dependencies added: list-t

Dependency ranges changed: z3

Files

• ChangeLog.md +4/−0
• expressions-z3.cabal +3/−2
• src/Data/Expression/Z3.hs +2/−2

@@ -1,5 +1,9 @@ # Revision history for expressions-z3 +## 0.1.4++* Bump dependencies+ ## 0.1.3  * Bump dependencies

@@ -1,5 +1,5 @@ name:                expressions-z3-version:             0.1.3+version:             0.1.4 synopsis:            Encode and Decode expressions from Z3 ASTs description:   A simple interface for converting expressions back and forth between pure@@ -67,7 +67,8 @@                        expressions >=0.1 && <0.2,                        singletons >=2.2 && <2.5,                        transformers >=0.5.2 && <0.6,-                       z3 >=4.1.2 && <4.3+                       list-t >=1.0 && <1.1,+                       z3 >=4.1.2 && <4.4   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns

@@ -16,7 +16,6 @@ import Control.Monad import Control.Monad.IO.Class import Control.Monad.Trans.Class-import Control.Monad.Trans.List import Control.Monad.Trans.State import Data.Expression import Data.List hiding (and, or)@@ -24,6 +23,7 @@ import Data.Proxy import Data.Singletons import Data.Singletons.Decide+import ListT hiding (head, null) import Prelude hiding (and, or, not)  import qualified Data.Functor.Const as F@@ -363,6 +363,6 @@         return e  fromZ3 :: forall (f :: (Sort -> *) -> Sort -> *) (s :: Sort) z3. ( IFromZ3 f, Z3.MonadZ3 z3, SingI s ) => Z3.AST -> z3 (IFix f s)-fromZ3 a = let r = ifromZ3 (Proxy :: Proxy f) r in head' <=< fmap (mapMaybe toStaticallySorted) . runListT . flip evalStateT M.empty . unwrap . r $ a where+fromZ3 a = let r = ifromZ3 (Proxy :: Proxy f) r in head' <=< fmap (mapMaybe toStaticallySorted) . toList . flip evalStateT M.empty . unwrap . r $ a where     head' (h : _) = return h     head' _       = Z3.astToString a >>= \s -> error ("couldn't re-encode Z3 AST: " ++ s)