liquid-fixpoint 0.2.1.0 → 0.2.1.1

raw patch · 4 files changed

+12/−21 lines, 4 filesdep ~basePVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• liquid-fixpoint.cabal +4/−4
• src/Language/Fixpoint/SmtLib2.hs +4/−10
• src/Language/Fixpoint/Sort.hs +2/−7
• src/Language/Fixpoint/Types.hs +2/−0

@@ -1,5 +1,5 @@ name:                liquid-fixpoint-version:             0.2.1.0+version:             0.2.1.1 Copyright:           2010-15 Ranjit Jhala, University of California, San Diego. synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage:            https://github.com/ucsd-progsys/liquid-fixpoint@@ -92,7 +92,7 @@ -- asked. Executable fixpoint.native   Main-is: Fixpoint.hs-  Build-Depends: base >= 4 && < 5+  Build-Depends: base >= 4.7 && < 5                , array                , syb                , cmdargs@@ -118,7 +118,7 @@  Executable fixpoint   Main-is:       Fixpoint.hs-  Build-Depends: base >= 4 && < 5+  Build-Depends: base >= 4.7 && < 5                , array                , syb                , cmdargs@@ -156,7 +156,7 @@                    Language.Fixpoint.SmtLib2,                    Language.Fixpoint.Misc   -  Build-Depends: base >= 4 && < 5+  Build-Depends: base >= 4.7 && < 5                , array                , attoparsec                , syb

@@ -44,9 +44,7 @@ import Language.Fixpoint.Files import Language.Fixpoint.Types -import Control.Arrow import Control.Monad-import Control.Monad.IO.Class import Data.Char import qualified Data.List as L import qualified Data.HashMap.Strict as M@@ -60,13 +58,9 @@ import System.Exit import System.FilePath import System.Process-import System.IO            (openFile, IOMode (..), Handle, hFlush, hClose, hReady)+import System.IO            (openFile, IOMode (..), Handle, hFlush, hClose) import Control.Applicative  ((<$>), (<|>), (*>), (<*)) -import Text.Parsec.Text.Lazy ()-import Text.Parsec.Char-import Text.Parsec.Combinator-import Text.Parsec.Prim (ParsecT, runPT, getState, setInput, try) import qualified Data.Attoparsec.Text as A  {- Usage:@@ -248,9 +242,9 @@ smtPreamble Z3 me    = do smtWrite me "(get-info :version)"        r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me-       case r of-         "4.3.2" -> return $ z3_432_options ++ z3Preamble-         _       -> return $ z3_options ++ z3Preamble+       case T.words r of+         "4.3.2" : _  -> return $ z3_432_options ++ z3Preamble+         _            -> return $ z3_options ++ z3Preamble smtPreamble _  _     = return smtlibPreamble 

@@ -149,9 +149,7 @@   = do tp <- checkPred f p        t1 <- checkExpr f e1        t2 <- checkExpr f e2-       if t1 == t2 -         then return t1-         else throwError (errIte e1 e2 t1 t2) +       ((`apply` t1) <$> unify [t1] [t2]) `catchError` (\_ -> throwError $ errIte e1 e2 t1 t2)  -- | Helper for checking cast expressions  @@ -159,10 +157,7 @@   = checkApp f (Just t) g es checkCst f t e              = do t' <- checkExpr f e-       if t == t' -         then return t-         else throwError (errCast e t' t)-+       ((`apply` t) <$> unify [t] [t']) `catchError` (\_ -> throwError $ errCast e t' t)  checkApp f to g es   = snd <$> checkApp' f to g es

@@ -63,6 +63,7 @@   , pAnd, pOr, pIte   , isTautoPred   , symConstLits+  , zero    -- * Generalizing Embedding with Typeclasses   , Symbolic (..)@@ -647,6 +648,7 @@ exprReft      = relReft Eq notExprReft   = relReft Ne uexprReft     = relReft Ueq+  -- exprReft e             = Reft (vv_, [RConc $ PAtom Eq (eVar vv_)  (expr e)]) -- notExprReft e          = Reft (vv_, [RConc $ PAtom Ne (eVar vv_)  (expr e)])