liquid-fixpoint 0.2.3.0 → 0.2.3.1
raw patch · 2 files changed
+19/−164 lines, 2 filesdep −QuickCheckdep −tastydep −tasty-quickcheckdep ~basePVP ok
version bump matches the API change (PVP)
Dependencies removed: QuickCheck, tasty, tasty-quickcheck, tasty-rerun
Dependency ranges changed: base
API changes (from Hackage documentation)
Files
- liquid-fixpoint.cabal +19/−19
- tests/test.hs +0/−145
liquid-fixpoint.cabal view
@@ -1,5 +1,5 @@ name: liquid-fixpoint-version: 0.2.3.0+version: 0.2.3.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@@ -183,21 +183,21 @@ , unordered-containers , text-format -test-suite test- default-language: Haskell98- type: exitcode-stdio-1.0- hs-source-dirs: tests- ghc-options: -O2 -threaded- main-is: test.hs- build-depends: base,- -- directory,- -- filepath,- -- process,- -- tagged,- liquid-fixpoint,- -- optparse-applicative == 0.11.*,- QuickCheck,- tasty >= 0.10,- tasty-quickcheck,- tasty-rerun >= 1.1,- text+-- test-suite test+-- default-language: Haskell98+-- type: exitcode-stdio-1.0+-- hs-source-dirs: tests+-- ghc-options: -O2 -threaded+-- main-is: test.hs+-- build-depends: base,+-- -- directory,+-- -- filepath,+-- -- process,+-- -- tagged,+-- liquid-fixpoint,+-- -- optparse-applicative == 0.11.*,+-- QuickCheck,+-- tasty >= 0.10,+-- tasty-quickcheck,+-- tasty-rerun >= 1.1,+-- text
− tests/test.hs
@@ -1,145 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}-module Main where--import Language.Fixpoint.Names-import Language.Fixpoint.Parse-import Language.Fixpoint.PrettyPrint-import Language.Fixpoint.Types--import Control.Monad-import Data.Proxy-import Data.Text (Text, cons, inits, pack)-import Test.QuickCheck-import Test.Tasty-import Test.Tasty.Ingredients.Rerun-import Test.Tasty.Options-import Test.Tasty.QuickCheck-import Test.Tasty.Runners--main :: IO ()-main = run tests - where- run = defaultMainWithIngredients [ - rerunningTests [ listingTests, consoleTestReporter ]- , includingOptions [ Option (Proxy :: Proxy QuickCheckTests)- ]- ]- - tests = testGroup "Tests" [ quickCheckTests ]--quickCheckTests :: TestTree-quickCheckTests- = testGroup "Properties"- [ testProperty "prop_pprint_parse_inv_expr" prop_pprint_parse_inv_expr- , testProperty "prop_pprint_parse_inv_pred" prop_pprint_parse_inv_pred- ]--prop_pprint_parse_inv_pred :: Pred -> Bool-prop_pprint_parse_inv_pred p = p == rr (showpp p)--prop_pprint_parse_inv_expr :: Expr -> Bool-prop_pprint_parse_inv_expr p = simplify p == rr (showpp $ simplify p)--instance Arbitrary Sort where- arbitrary = sized arbSort--arbSort 0 = oneof [return FInt, return FReal, return FNum]-arbSort n = frequency- [(1, return FInt)- ,(1, return FReal)- ,(1, return FNum)- ,(2, fmap FObj arbitrary)- ]---instance Arbitrary Pred where- arbitrary = sized arbPred- shrink = filter valid . genericShrink- where- valid (PAnd []) = False- valid (PAnd [_]) = False- valid (POr []) = False- valid (POr [_]) = False- valid (PBexp (EBin _ _ _)) = True- valid (PBexp _) = False- valid _ = True--arbPred 0 = elements [PTrue, PFalse]-arbPred n = frequency- [(1, return PTrue)- ,(1, return PFalse)- ,(2, fmap PAnd twoPreds)- ,(2, fmap POr twoPreds)- ,(2, fmap PNot (arbPred (n `div` 2)))- ,(2, liftM2 PImp (arbPred (n `div` 2)) (arbPred (n `div` 2)))- ,(2, liftM2 PIff (arbPred (n `div` 2)) (arbPred (n `div` 2)))- ,(2, fmap PBexp (arbExpr (n `div` 2)))- ,(2, liftM3 PAtom arbitrary (arbExpr (n `div` 2)) (arbExpr (n `div` 2)))- -- ,liftM2 PAll arbitrary arbitrary- -- ,return PTop- ]- where- twoPreds = do- x <- arbPred (n `div` 2)- y <- arbPred (n `div` 2)- return [x,y]--instance Arbitrary Expr where- arbitrary = sized arbExpr- shrink = filter valid . genericShrink- where valid (EApp _ []) = False- valid _ = True--arbExpr 0 = oneof [fmap ESym arbitrary, fmap ECon arbitrary, fmap EVar arbitrary, return EBot]-arbExpr n = frequency- [(1, fmap ESym arbitrary)- ,(1, fmap ECon arbitrary)- ,(1, fmap EVar arbitrary)- ,(1, return EBot)- -- ,liftM2 ELit arbitrary arbitrary -- restrict literals somehow- ,(2, choose (1,3) >>= \m -> liftM2 EApp arbitrary (vectorOf m (arbExpr (n `div` 2)))) - ,(2, liftM3 EBin arbitrary (arbExpr (n `div` 2)) (arbExpr (n `div` 2)))- ,(2, liftM3 EIte (arbPred (max 2 (n `div` 2)) `suchThat` isRel)- (arbExpr (n `div` 2))- (arbExpr (n `div` 2)))- ,(2, liftM2 ECst (arbExpr (n `div` 2)) (arbSort (n `div` 2)))- ]- where- isRel (PAtom _ _ _) = True- isRel _ = False--instance Arbitrary Brel where- arbitrary = oneof (map return [Eq, Ne, Gt, Ge, Lt, Le, Ueq, Une])--instance Arbitrary Bop where- arbitrary = oneof (map return [Plus, Minus, Times, Div, Mod])--instance Arbitrary SymConst where- arbitrary = fmap SL arbitrary--instance Arbitrary Symbol where- arbitrary = fmap (symbol :: Text -> Symbol) arbitrary--instance Arbitrary Text where- arbitrary = choose (1,4) >>= \n ->- fmap pack (vectorOf n char `suchThat` valid)- where- char = elements ['a'..'z']- valid x = x `notElem` fixpointNames && not (isFixKey x)--instance Arbitrary FTycon where- arbitrary = do- c <- elements ['A'..'Z']- t <- arbitrary- return $ symbolFTycon $ dummyLoc $ symbol $ cons c t--instance Arbitrary Constant where- arbitrary = oneof [fmap I (arbitrary `suchThat` (>=0))- -- ,fmap R arbitrary- ]- shrink = genericShrink--instance Arbitrary a => Arbitrary (Located a) where- arbitrary = fmap dummyLoc arbitrary- shrink = fmap dummyLoc . shrink . val