expressions 0.1.4 → 0.1.5

raw patch · 5 files changed

+43/−22 lines, 5 filesdep −QuickCheckdep −tastydep −tasty-quickcheckdep ~basedep ~containersdep ~singletonssetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: QuickCheck, tasty, tasty-quickcheck

Dependency ranges changed: base, containers, singletons

API changes (from Hackage documentation)

Files

• ChangeLog.md +4/−0
• Setup.hs +0/−2
• expressions.cabal +5/−8
• src/Data/Expression/Arithmetic.hs +4/−3
• test/Main.hs +30/−9

@@ -1,5 +1,9 @@ # Change Log +## 0.1.5++* Bump dependencies, fix equality, tweak readme+ ## 0.1.4  * Bump dependencies

@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain

@@ -1,5 +1,5 @@ name:                expressions-version:             0.1.4+version:             0.1.5 synopsis:            Expressions and Formulae a la carte description:   This package is aimed at providing means of fixing a first-order language and@@ -71,10 +71,10 @@                        TypeSynonymInstances,                        UndecidableInstances   build-depends:       attoparsec >=0.13 && <0.14,-                       base >=4.9 && <4.11,-                       containers >=0.5.7 && <0.5.11,+                       base >=4.9 && <4.12,+                       containers >=0.5.7 && <0.6,                        lattices >=1.6 && <1.8,-                       singletons >=2.2 && <2.4,+                       singletons >=2.2 && <2.5,                        text >=1.2 && <1.3,                        transformers >=0.5.2 && <0.6   hs-source-dirs:      src@@ -86,10 +86,7 @@   build-depends:       base,                        expressions,                        singletons,-                       text,-                       tasty,-                       tasty-quickcheck,-                       QuickCheck >=2.10 && <2.11+                       text   hs-source-dirs:      test   main-is:             Main.hs   default-language:    Haskell2010

@@ -53,9 +53,10 @@     LessThan :: a 'IntegralSort -> a 'IntegralSort -> ArithmeticF a 'BooleanSort  instance IEq1 ArithmeticF where-    Const a  `ieq1` Const b  = a == b-    Add   as `ieq1` Add   bs = foldr (&&) True $ zipWith ieq as bs-    Mul   as `ieq1` Mul   bs = foldr (&&) True $ zipWith ieq as bs+    Const a  `ieq1` Const b = a == b++    Add as `ieq1` Add bs | length as == length bs = foldr (&&) True $ zipWith ieq as bs+    Mul as `ieq1` Mul bs | length as == length bs = foldr (&&) True $ zipWith ieq as bs      Divides  c a `ieq1` Divides  d b = a `ieq` b && c == d     LessThan a c `ieq1` LessThan b d = a `ieq` b && c `ieq` d

@@ -1,26 +1,47 @@ {-# LANGUAGE DataKinds+           , FlexibleContexts            , KindSignatures            , OverloadedStrings            , RankNTypes            , TypeOperators #-} +import Control.Monad import Data.Maybe import Data.Singletons import Data.Text import Prelude hiding (and)-import Test.QuickCheck hiding ((.&.))-import Test.Tasty-import Test.Tasty.QuickCheck hiding ((.&.)) +import qualified Prelude as P+ import Data.Expression  parseJust :: forall f (s :: Sort). ( Parseable f f, SingI s ) => Text -> IFix f s parseJust = fromJust . parse +a, b, x, y, z :: forall f (s :: Sort). ( VarF :<: f, SingI s ) => IFix f s+a = var "a"+b = var "b"+x = var "x"+y = var "y"+z = var "z"++c1, c3 :: forall f. ArithmeticF :<: f => IFix f 'IntegralSort+c1 = cnst 1+c3 = cnst 3+ main :: IO ()-main = defaultMain $ testGroup "parsing" [ testProperty "1" $ once $ var "a" == (parseJust "(a : int)" :: ALia 'IntegralSort)-                                         , testProperty "2" $ once $ var "a" /= (parseJust "(+ (a : int) 3)" :: ALia 'IntegralSort)-                                         , testProperty "3" $ once $ var "a" .+. cnst 1 == (parseJust "(+ (a : int) 1)" :: ALia 'IntegralSort)-                                         , testProperty "4" $ once $ select (var "a") (var "b" .+. cnst 3) == (parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))" :: QFALia ('ArraySort 'IntegralSort 'BooleanSort))-                                         , testProperty "5" $ once $ forall [var "x" :: Var 'IntegralSort] (exists [var "y" :: Var 'IntegralSort] (and [true, var "b" .=. (var "x" .<. var "y")])) == (parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))" :: Lia 'BooleanSort)-                                         , testProperty "6" $ once $ forall [var "x" :: Var 'IntegralSort, var "y"] (var "x" .<. var "y" .+. var "z") .&. var "z" .=. cnst 3 == (parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))" :: Lia 'BooleanSort) ]+main = guard (P.and props) where++    props = [ e1 == (parseJust "(a : int)"                                                                   :: ALia 'IntegralSort)+            , e2 /= (parseJust "(+ (a : int) 3)"                                                             :: ALia 'IntegralSort)+            , e3 == (parseJust "(+ (a : int) 1)"                                                             :: ALia 'IntegralSort)+            , e4 == (parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))"                   :: QFALia ('ArraySort 'IntegralSort 'BooleanSort))+            , e5 == (parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))" :: Lia 'BooleanSort)+            , e6 == (parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"          :: Lia 'BooleanSort) ]++    e1 = a+    e2 = a+    e3 = a .+. c1+    e4 = select a (b .+. c3)+    e5 = forall [x :: Var 'IntegralSort] (exists [y :: Var 'IntegralSort] (and [true, b .=. (x .<. y)]))+    e6 = forall [x :: Var 'IntegralSort, y] (x .<. y .+. z) .&. z .=. c3