diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2014 Oleg Grenrus + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,15 @@ +# Boolean normal forms + +[![Build Status](https://travis-ci.org/phadej/boolean-normal-forms.svg?branch=master)](https://travis-ci.org/phadej/boolean-normal-forms) + +This library provides types that might be useful in symbolic manipulation of propositional logic expressions. + +## Features + +- **CNF** (list and set) +- **DNF** (list and set) +- **NNF** (tree and set) +- FreeBoolean type useful in testing + +Distributed under MIT license +© Oleg Grenrus 2014 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/boolean-normal-forms.cabal b/boolean-normal-forms.cabal new file mode 100644 --- /dev/null +++ b/boolean-normal-forms.cabal @@ -0,0 +1,70 @@ +name: boolean-normal-forms +version: 0.0.0.1 +synopsis: Boolean normal form: NNF, DNF & CNF +description: The provided types that might be useful in symbolic manipulation of propositional logic expressions. +license: MIT +license-file: LICENSE +author: Oleg Grenrus +maintainer: oleg.grenrus@iki.fi +copyright: © Oleg Grenrus 2014 +category: Data +build-type: Simple +cabal-version: >=1.10 +extra-source-files: README.md +extra-doc-files: doc-formulae/*.svg + +library + hs-source-dirs: src + exposed-modules: Data.Algebra.Boolean.NormalForm, + Data.Algebra.Boolean.FreeBoolean, + Data.Algebra.Boolean.NNF, + Data.Algebra.Boolean.DNF, + Data.Algebra.Boolean.CNF, + Data.Algebra.Boolean.Negable, + Data.Algebra.Boolean.CoBoolean, + Data.Algebra.Boolean.NNF.Set, + Data.Algebra.Boolean.NNF.Tree, + Data.Algebra.Boolean.DNF.List, + Data.Algebra.Boolean.DNF.Set, + Data.Algebra.Boolean.CNF.List, + Data.Algebra.Boolean.CNF.Set + other-extensions: DeriveFunctor, + DeriveDataTypeable, + ConstraintKinds, + TypeFamilies, + ScopedTypeVariables + build-depends: base >=4.6 && <4.8, + containers >=0.5 && <0.6, + cond >=0.4.1 && <0.5 + default-language: Haskell2010 + ghc-options: -Wall + -O2 + -fwarn-tabs + -fspec-constr-count=6 + -fmax-simplifier-iterations=10 + -fdicts-cheap + +test-suite test + default-language: Haskell2010 + type: exitcode-stdio-1.0 + hs-source-dirs: tests + main-is: Main.hs + other-modules: BooleanLaws, + CNFList, + CNFSet, + DNFList, + DNFSet, + FreeBoolean, + FreeBooleanTests, + NegableLaws, + NNFSet, + NNFTree, + SimplifyLaws + ghc-options: -Wall -O2 -fno-warn-orphans + build-depends: base >=4.6 && <4.8, + containers >= 0.5 && <0.6, + cond >=0.4.1 && <0.5, + tasty >=0.8, + tasty-quickcheck >=0.8.0.3, + QuickCheck >=2.7 && <=2.8, + boolean-normal-forms diff --git a/doc-formulae/cnf.svg b/doc-formulae/cnf.svg new file mode 100644 --- /dev/null +++ b/doc-formulae/cnf.svg @@ -0,0 +1,22 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc-formulae/dnf.svg b/doc-formulae/dnf.svg new file mode 100644 --- /dev/null +++ b/doc-formulae/dnf.svg @@ -0,0 +1,22 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/doc-formulae/nnf.svg b/doc-formulae/nnf.svg new file mode 100644 --- /dev/null +++ b/doc-formulae/nnf.svg @@ -0,0 +1,59 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Data/Algebra/Boolean/CNF.hs b/src/Data/Algebra/Boolean/CNF.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/CNF.hs @@ -0,0 +1,15 @@ +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-- This module re-exports 'Set'-based implementation. +-------------------------------------------------------------------- +module Data.Algebra.Boolean.CNF ( + module Data.Algebra.Boolean.CNF.Set +) where + +import Data.Algebra.Boolean.CNF.Set diff --git a/src/Data/Algebra/Boolean/CNF/List.hs b/src/Data/Algebra/Boolean/CNF/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/CNF/List.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.CNF.List ( + CNF(..), + fromDoubleList, + toDoubleList, + fromNNF, + module Data.Algebra.Boolean.NormalForm + ) where + +import Prelude hiding ((||),(&&),not,any,all,and,or) +import Data.Monoid +import Data.Either (partitionEithers) +import Data.Typeable + +import Data.Algebra.Boolean.NormalForm +import Data.Algebra.Boolean.Negable hiding (not) +import qualified Data.Algebra.Boolean.Negable as Negable + +import Data.Algebra.Boolean.NNF.Tree + +import Data.Algebra.Boolean + +-- | Boolean formula in Conjunction Normal Form +-- +-- <> +newtype CNF a = CNF { unCNF :: [[a]] } + deriving (Eq, Ord, Show, Read, Functor, Typeable) + +instance CoBoolean1 CNF where + toBooleanWith f = all (any f) . unCNF + +instance CoBoolean a => CoBoolean (CNF a) where + toBoolean = toBooleanWith toBoolean + +fromDoubleList :: [[a]] -> CNF a +fromDoubleList = CNF + +toDoubleList :: CNF a -> [[a]] +toDoubleList = unCNF + +cnfNot :: Negable a => CNF a -> CNF a +cnfNot = any and . map (map $ toNormalForm . Negable.not) . unCNF + +instance Negable a => Negable (CNF a) where + not = cnfNot + +instance Negable a => Boolean (CNF a) where + false = CNF [[]] + true = CNF [] + (CNF a) && (CNF b) = CNF (a <> b) + (CNF a) || (CNF b) = CNF [ a' <> b' | a' <- a, b' <- b ] + not = cnfNot + +fromNNF :: Negable a => NNF a -> CNF a +fromNNF = toBooleanWith toNormalForm + +instance NormalForm CNF where + type NFConstraint CNF a = Negable a + + toNormalForm x = CNF [[x]] + + simplify f = CNF . p . g . map (h . map f') . unCNF + where f' x = case f x of + Just b -> Right b + Nothing -> Left x + h :: [Either a Bool] -> Either [a] Bool + h disj | True `elem` r = Right True + | null l = Right False + | otherwise = Left l + where (l, r) = partitionEithers disj + g :: [Either a Bool] -> Either [a] Bool + g conj | False `elem` r = Right False + | null l = Right True + | otherwise = Left l + where (l, r) = partitionEithers conj + p :: Either [[a]] Bool -> [[a]] + p (Right True) = [] + p (Right False) = [[]] + p (Left x) = x + + fromFreeBoolean = fromNNF . toBooleanWith toNormalForm diff --git a/src/Data/Algebra/Boolean/CNF/Set.hs b/src/Data/Algebra/Boolean/CNF/Set.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/CNF/Set.hs @@ -0,0 +1,105 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.CNF.Set ( + CNF(..), + fromDoubleList, + toDoubleList, + fromNNF, + module Data.Algebra.Boolean.NormalForm + ) where + +import Prelude hiding ((||),(&&),not,and,or,any,all) +import Data.Monoid +import Data.Typeable + +import Data.Set (Set) +import qualified Data.Set as Set + +import Data.List (sortBy, foldl') +import Data.Function (on) + +import Data.Algebra.Boolean.NormalForm +import Data.Algebra.Boolean.Negable hiding (not) +import qualified Data.Algebra.Boolean.Negable as Negable + +import Data.Algebra.Boolean.NNF.Tree + +import Data.Algebra.Boolean + +-- | Boolean formula in Conjunction Normal Form +-- +-- <> +newtype CNF a = CNF { unCNF :: Set (Set a) } + deriving (Eq, Ord, Show, Read, Typeable) + +instance CoBoolean1 CNF where + toBooleanWith f = all (any f) . unCNF + +instance CoBoolean a => CoBoolean (CNF a) where + toBoolean = toBooleanWith toBoolean + +toDoubleList :: CNF a -> [[a]] +toDoubleList = map Set.toList . Set.toList . unCNF + +fromDoubleList :: (Ord a) => [[a]] -> CNF a +fromDoubleList = CNF . Set.fromList . map Set.fromList + +cnfNot :: (Ord a, Negable a) => CNF a -> CNF a +cnfNot = any and . map (map $ toNormalForm . Negable.not) . toDoubleList + +instance (Ord a, Negable a) => Negable (CNF a) where + not = cnfNot + +instance (Ord a, Negable a) => Boolean (CNF a) where + false = CNF $ Set.singleton Set.empty + true = CNF Set.empty + (CNF a) && (CNF b) = CNF (a <> b) + (CNF a) || (CNF b) = CNF $ Set.fromList [a' <> b' | a' <- Set.toList a, b' <- Set.toList b ] + not = cnfNot + +fromLeft :: Either a b -> a +fromLeft (Left x) = x +fromLeft _ = error "fromLeft called on Right value" + +optimize :: Ord a => Set (Set a) -> Set (Set a) +optimize = Set.fromList . f . sortBy (flip compare `on` Set.size) . Set.toList + where f disj = foldl' g disj disj + g disj item = filter (not . Set.isProperSubsetOf item) disj + +fromNNF :: (Ord a, Negable a) => NNF a -> CNF a +fromNNF = toBooleanWith toNormalForm + +instance NormalForm CNF where + type NFConstraint CNF a = (Negable a, Ord a) + + toNormalForm = CNF . Set.singleton . Set.singleton + + simplify f = CNF . optimize . p . g . Set.map h . Set.map (Set.map f') . unCNF + where f' x = case f x of + Just b -> Right b + Nothing -> Left x + h :: Ord a => Set (Either a Bool) -> Either (Set a) Bool + h disj | Right True `Set.member` disj = Right True + | Set.null l = Right False + | otherwise = Left l + where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) disj + g :: Ord a => Set (Either a Bool) -> Either (Set a) Bool + g conj | Right False `Set.member` conj = Right False + | Set.null l = Right True + | otherwise = Left l + where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) conj + p :: Either (Set (Set a)) Bool -> Set (Set a) + p (Right True) = Set.empty + p (Right False) = Set.singleton Set.empty + p (Left x) = x + + fromFreeBoolean = fromNNF . toBooleanWith toNormalForm diff --git a/src/Data/Algebra/Boolean/CoBoolean.hs b/src/Data/Algebra/Boolean/CoBoolean.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/CoBoolean.hs @@ -0,0 +1,50 @@ +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.CoBoolean ( + CoBoolean(..), + CoBoolean1(..), + toBool, + toBoolWith +) where + +import Data.Algebra.Boolean + +-- | A class to values translable to booleans. +class CoBoolean a where + -- | Cast value to 'Boolean'. + toBoolean :: Boolean b => a -> b + +-- | Less polymorphic version of 'toBoolean'. +toBool :: CoBoolean a => a -> Bool +toBool = toBoolean + +-- | A polymorphic class of values translable to booleans. +class CoBoolean1 b where + -- | Cast value to 'Boolean'. + toBooleanWith :: Boolean c => (a -> c) -> b a -> c + +-- | Less polymorphic version of 'toBooleanWith'. +toBoolWith :: CoBoolean1 b => (a -> Bool) -> b a -> Bool +toBoolWith = toBooleanWith + +instance CoBoolean Bool where + toBoolean = fromBool + +instance (CoBoolean f, CoBoolean g) => CoBoolean (Either f g) where + toBoolean (Left x) = toBoolean x + toBoolean (Right x) = toBoolean x + +instance CoBoolean (Maybe a) where + toBoolean (Just _) = true + toBoolean Nothing = false + +instance CoBoolean1 Maybe where + toBooleanWith f (Just x) = f x + toBooleanWith _ Nothing = false diff --git a/src/Data/Algebra/Boolean/DNF.hs b/src/Data/Algebra/Boolean/DNF.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/DNF.hs @@ -0,0 +1,15 @@ +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-- This module re-exports 'Set'-based implementation. +-------------------------------------------------------------------- +module Data.Algebra.Boolean.DNF ( + module Data.Algebra.Boolean.DNF.Set +) where + +import Data.Algebra.Boolean.DNF.Set diff --git a/src/Data/Algebra/Boolean/DNF/List.hs b/src/Data/Algebra/Boolean/DNF/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/DNF/List.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.DNF.List ( + DNF(..), + fromDoubleList, + toDoubleList, + fromNNF, + module Data.Algebra.Boolean.NormalForm + ) where + +import Prelude hiding ((||),(&&),not,any,all,and,or) +import Data.Monoid +import Data.Either (partitionEithers) +import Data.Typeable + +import Data.Algebra.Boolean.NormalForm +import Data.Algebra.Boolean.Negable hiding (not) +import qualified Data.Algebra.Boolean.Negable as Negable + +import Data.Algebra.Boolean.NNF.Tree + +import Data.Algebra.Boolean + +-- | Boolean formula in Disjunction Normal Form +-- +-- <> +newtype DNF a = DNF { unDNF :: [[a]] } + deriving (Eq, Ord, Show, Read, Functor, Typeable) + +instance CoBoolean1 DNF where + toBooleanWith f = any (all f) . unDNF + +instance CoBoolean a => CoBoolean (DNF a) where + toBoolean = toBooleanWith toBoolean + +fromDoubleList :: [[a]] -> DNF a +fromDoubleList = DNF + +toDoubleList :: DNF a -> [[a]] +toDoubleList = unDNF + +dnfNot :: Negable a => DNF a -> DNF a +dnfNot = all or . map (map $ toNormalForm . Negable.not) . unDNF + +instance Negable a => Negable (DNF a) where + not = dnfNot + +instance Negable a => Boolean (DNF a) where + true = DNF [[]] + false = DNF [] + (DNF a) || (DNF b) = DNF (a <> b) + (DNF a) && (DNF b) = DNF [ a' <> b' | a' <- a, b' <- b ] + not = dnfNot + +fromNNF :: Negable a => NNF a -> DNF a +fromNNF = toBooleanWith toNormalForm + +instance NormalForm DNF where + type NFConstraint DNF a = Negable a + + toNormalForm x = DNF [[x]] + + simplify f = DNF . q . h . map (g . map f') . unDNF + where f' x = case f x of + Just b -> Right b + Nothing -> Left x + h :: [Either a Bool] -> Either [a] Bool + h disj | True `elem` r = Right True + | null l = Right False + | otherwise = Left l + where (l, r) = partitionEithers disj + g :: [Either a Bool] -> Either [a] Bool + g conj | False `elem` r = Right False + | null l = Right True + | otherwise = Left l + where (l, r) = partitionEithers conj + q :: Either [[a]] Bool -> [[a]] + q (Right True) = [[]] + q (Right False) = [] + q (Left x) = x + + fromFreeBoolean = fromNNF . toBooleanWith toNormalForm diff --git a/src/Data/Algebra/Boolean/DNF/Set.hs b/src/Data/Algebra/Boolean/DNF/Set.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/DNF/Set.hs @@ -0,0 +1,105 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.DNF.Set ( + DNF(..), + fromDoubleList, + toDoubleList, + fromNNF, + module Data.Algebra.Boolean.NormalForm + ) where + +import Prelude hiding ((||),(&&),not,and,or,any,all) +import Data.Monoid +import Data.Typeable + +import Data.Set (Set) +import qualified Data.Set as Set + +import Data.List (sortBy, foldl') +import Data.Function (on) + +import Data.Algebra.Boolean.NormalForm +import Data.Algebra.Boolean.Negable hiding (not) +import qualified Data.Algebra.Boolean.Negable as Negable + +import Data.Algebra.Boolean.NNF.Tree + +import Data.Algebra.Boolean + +-- | Boolean formula in Disjunction Normal Form +-- +-- <> +newtype DNF a = DNF { unDNF :: Set (Set a) } + deriving (Eq, Ord, Show, Read, Typeable) + +instance CoBoolean1 DNF where + toBooleanWith f = any (all f) . unDNF + +instance CoBoolean a => CoBoolean (DNF a) where + toBoolean = toBooleanWith toBoolean + +toDoubleList :: DNF a -> [[a]] +toDoubleList = map Set.toList . Set.toList . unDNF + +fromDoubleList :: (Ord a) => [[a]] -> DNF a +fromDoubleList = DNF . Set.fromList . map Set.fromList + +dnfNot :: (Ord a, Negable a) => DNF a -> DNF a +dnfNot = all or . map (map $ toNormalForm . Negable.not) . toDoubleList + +instance (Ord a, Negable a) => Negable (DNF a) where + not = dnfNot + +instance (Ord a, Negable a) => Boolean (DNF a) where + true = DNF $ Set.singleton Set.empty + false = DNF Set.empty + (DNF a) || (DNF b) = DNF (a <> b) + (DNF a) && (DNF b) = DNF $ Set.fromList [a' <> b' | a' <- Set.toList a, b' <- Set.toList b ] + not = dnfNot + +fromLeft :: Either a b -> a +fromLeft (Left x) = x +fromLeft _ = error "fromLeft called on Right value" + +optimize :: Ord a => Set (Set a) -> Set (Set a) +optimize = Set.fromList . f . sortBy (compare `on` Set.size) . Set.toList + where f conj = foldl' g conj conj + g conj item = filter (not . Set.isProperSubsetOf item) conj + +fromNNF :: (Ord a, Negable a) => NNF a -> DNF a +fromNNF = toBooleanWith toNormalForm + +instance NormalForm DNF where + type NFConstraint DNF a = (Negable a, Ord a) + + toNormalForm = DNF . Set.singleton . Set.singleton + + simplify f = DNF . optimize . q . h . Set.map g . Set.map (Set.map f') . unDNF + where f' x = case f x of + Just b -> Right b + Nothing -> Left x + h :: Ord a => Set (Either a Bool) -> Either (Set a) Bool + h disj | Right True `Set.member` disj = Right True + | Set.null l = Right False + | otherwise = Left l + where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) disj + g :: Ord a => Set (Either a Bool) -> Either (Set a) Bool + g conj | Right False `Set.member` conj = Right False + | Set.null l = Right True + | otherwise = Left l + where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) conj + q :: Either (Set (Set a)) Bool -> Set (Set a) + q (Right True) = Set.singleton Set.empty + q (Right False) = Set.empty + q (Left x) = x + + fromFreeBoolean = fromNNF . toBooleanWith toNormalForm diff --git a/src/Data/Algebra/Boolean/FreeBoolean.hs b/src/Data/Algebra/Boolean/FreeBoolean.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/FreeBoolean.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveDataTypeable #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.FreeBoolean ( + FreeBoolean(..), + module Data.Algebra.Boolean.CoBoolean +) where + +import Data.Typeable + +import Data.Algebra.Boolean.CoBoolean +import Data.Algebra.Boolean.Negable hiding (not) +import qualified Data.Algebra.Boolean.Negable as Negable + +import Prelude hiding ((||),(&&),not,any,all) +import Data.Algebra.Boolean + +-- | Free 'Boolean' type, does not perform any optimizations on the structure. Useful only in tests. +-- +-- Consider using 'Data.Algebra.Boolean.NNF'. +data FreeBoolean a = FBValue a + | FBTrue + | FBFalse + | FBNot (FreeBoolean a) + | FBAnd (FreeBoolean a) (FreeBoolean a) + | FBOr (FreeBoolean a) (FreeBoolean a) + deriving (Eq, Ord, Show, Read, Functor, Typeable) + +instance CoBoolean1 FreeBoolean where + toBooleanWith f (FBValue x) = f x + toBooleanWith _ FBTrue = true + toBooleanWith _ FBFalse = false + toBooleanWith f (FBNot x) = not $ toBooleanWith f x + toBooleanWith f (FBOr a b) = toBooleanWith f a || toBooleanWith f b + toBooleanWith f (FBAnd a b) = toBooleanWith f a && toBooleanWith f b + +instance CoBoolean a => CoBoolean (FreeBoolean a) where + toBoolean = toBooleanWith toBoolean + +instance Negable (FreeBoolean a) where + not = FBNot + +instance Boolean (FreeBoolean a) where + true = FBTrue + false = FBFalse + (||) = FBOr + (&&) = FBAnd + not = FBNot diff --git a/src/Data/Algebra/Boolean/NNF.hs b/src/Data/Algebra/Boolean/NNF.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/NNF.hs @@ -0,0 +1,15 @@ +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-- This module re-exports tree-based implementation. +-------------------------------------------------------------------- +module Data.Algebra.Boolean.NNF ( + module Data.Algebra.Boolean.NNF.Tree +) where + +import Data.Algebra.Boolean.NNF.Tree diff --git a/src/Data/Algebra/Boolean/NNF/Set.hs b/src/Data/Algebra/Boolean/NNF/Set.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/NNF/Set.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.NNF.Set ( + NNF(..), + module Data.Algebra.Boolean.NormalForm + ) where + +import Data.Set (Set) +import qualified Data.Set as Set + +import Data.Algebra.Boolean.NormalForm +import Data.Algebra.Boolean.Negable hiding (not) +import qualified Data.Algebra.Boolean.Negable as Negable + +import Prelude hiding ((||),(&&),not,any,all) +import Data.Algebra.Boolean + +import Data.Typeable + +-- | Boolean formula in Negation Normal Form +-- +-- 'Boolean' operations will perform transformations as below: +-- +-- <> +data NNF a = NNFTrue + | NNFFalse + | NNFValue a + | NNFOr (Set (NNF a)) + | NNFAnd (Set (NNF a)) + deriving (Eq, Ord, Show, Read, Typeable) + +instance CoBoolean a => CoBoolean (NNF a) where + toBoolean = toBooleanWith toBoolean + +instance CoBoolean1 NNF where + toBooleanWith _ NNFTrue = true + toBooleanWith _ NNFFalse = false + toBooleanWith f (NNFValue x) = f x + toBooleanWith f (NNFOr xs) = any (toBooleanWith f) xs + toBooleanWith f (NNFAnd xs) = all (toBooleanWith f) xs + +orList :: Ord a => [NNF a] -> NNF a +orList x + | Set.null s = NNFFalse + | Set.member NNFTrue s = NNFTrue + | otherwise = NNFOr s + where s = Set.fromList $ filter (/= NNFFalse) $ concatMap g x + g (NNFOr xs) = concatMap g $ Set.toList xs + g y = [y] + +andList :: Ord a => [NNF a] -> NNF a +andList x + | Set.null s = NNFTrue + | Set.member NNFFalse s = NNFFalse + | otherwise = NNFAnd s + where s = Set.fromList $ filter (/= NNFTrue) $ concatMap g x + g (NNFAnd xs) = concatMap g $ Set.toList xs + g y = [y] + +nnfNot :: (Negable a, Ord a) => NNF a -> NNF a +nnfNot NNFTrue = NNFFalse +nnfNot NNFFalse = NNFTrue +nnfNot (NNFValue x) = NNFValue $ Negable.not x +nnfNot (NNFOr xs) = NNFAnd $ Set.map not xs +nnfNot (NNFAnd xs) = NNFOr $ Set.map not xs + +instance (Ord a, Negable a) => Negable (NNF a) where + not = nnfNot + +instance (Ord a, Negable a) => Boolean (NNF a) where + true = NNFTrue + false = NNFFalse + + a || b = orList [a, b] + a && b = andList [a, b] + + not = nnfNot + +instance NormalForm NNF where + type NFConstraint NNF a = (Ord a, Negable a) + + toNormalForm = NNFValue + + simplify f (NNFValue x) = case f x of + Just True -> NNFTrue + Just False -> NNFFalse + Nothing -> NNFValue x + simplify _ NNFTrue = NNFTrue + simplify _ NNFFalse = NNFFalse + simplify f (NNFAnd xs) = andList $ map (simplify f) $ Set.toList xs + simplify f (NNFOr xs) = orList $ map (simplify f) $ Set.toList xs + + fromFreeBoolean = toBooleanWith toNormalForm diff --git a/src/Data/Algebra/Boolean/NNF/Tree.hs b/src/Data/Algebra/Boolean/NNF/Tree.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/NNF/Tree.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.NNF.Tree ( + NNF(..), + module Data.Algebra.Boolean.NormalForm + ) where + +import Prelude hiding ((||),(&&),not) + +import Data.Algebra.Boolean.NormalForm +import Data.Algebra.Boolean.Negable hiding (not) +import qualified Data.Algebra.Boolean.Negable as Negable + +import Data.Algebra.Boolean + +import Data.Typeable + +-- | Boolean formula in Negation Normal Form +-- +-- 'Boolean' operations will perform transformations as below: +-- +-- <> +data NNF a = NNFTrue + | NNFFalse + | NNFValue a + | NNFOr (NNF a) (NNF a) + | NNFAnd (NNF a) (NNF a) + deriving (Eq, Ord, Show, Read, Functor, Typeable) + +instance CoBoolean a => CoBoolean (NNF a) where + toBoolean = toBooleanWith toBoolean + +instance CoBoolean1 NNF where + toBooleanWith _ NNFTrue = true + toBooleanWith _ NNFFalse = false + toBooleanWith f (NNFValue x) = f x + toBooleanWith f (NNFOr a b) = toBooleanWith f a || toBooleanWith f b + toBooleanWith f (NNFAnd a b) = toBooleanWith f a && toBooleanWith f b + +nnfNot :: Negable a => NNF a -> NNF a +nnfNot (NNFTrue) = NNFFalse +nnfNot NNFFalse = NNFTrue +nnfNot (NNFValue x) = NNFValue $ Negable.not x +nnfNot (NNFOr a b) = NNFAnd (not a) (not b) +nnfNot (NNFAnd a b) = NNFOr (not a) (not b) + +nnfOr :: NNF a -> NNF a -> NNF a +nnfOr NNFTrue _ = NNFTrue +nnfOr _ NNFTrue = NNFTrue +nnfOr NNFFalse NNFFalse = NNFFalse +nnfOr a b = NNFOr a b + +nnfAnd :: NNF a -> NNF a -> NNF a +nnfAnd NNFFalse _ = NNFFalse +nnfAnd _ NNFFalse = NNFFalse +nnfAnd NNFTrue NNFTrue = NNFTrue +nnfAnd a b = NNFAnd a b + +instance Negable a => Negable (NNF a) where + not = nnfNot + +instance Negable a => Boolean (NNF a) where + true = NNFTrue + false = NNFFalse + (||) = nnfOr + (&&) = nnfAnd + not = nnfNot + +instance NormalForm NNF where + type NFConstraint NNF a = Negable a + + toNormalForm = NNFValue + + simplify f (NNFValue x) = case f x of + Just True -> NNFTrue + Just False -> NNFFalse + Nothing -> NNFValue x + simplify _ NNFTrue = NNFTrue + simplify _ NNFFalse = NNFFalse + simplify f (NNFAnd a b) = nnfAnd (simplify f a) (simplify f b) + simplify f (NNFOr a b) = nnfOr (simplify f a) (simplify f b) + + fromFreeBoolean = toBooleanWith toNormalForm diff --git a/src/Data/Algebra/Boolean/Negable.hs b/src/Data/Algebra/Boolean/Negable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/Negable.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveDataTypeable #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.Negable ( + Neg(..), + Negable(..) +) + where + +import Data.Algebra.Boolean.CoBoolean + +import Data.Monoid +import Data.Typeable + +import Prelude hiding (not) +import qualified Prelude as P + +import qualified Data.Algebra.Boolean as B + +-- | Free 'Negable'. +data Neg a = Pos a -- ^ Positive value + | Neg a -- ^ Negative value + deriving (Eq, Ord, Show, Read, Functor, Typeable) + +instance CoBoolean (Neg a) where + toBoolean (Pos _) = B.true + toBoolean (Neg _) = B.false + +instance CoBoolean1 Neg where + toBooleanWith f (Pos x) = f x + toBooleanWith f (Neg x) = B.not $ f x + +-- | Class to represent invertible values. +-- +-- Must obey the double negation law: @not (not x) = x@ +-- +-- The negation appears only in leafs of normal forms, and the underlying proposition class +-- might have built-in negation, thus we use 'Negable'. +class Negable x where + -- | Invert the value. + not :: x -> x + +instance Negable (Neg a) where + not (Pos x) = Neg x + not (Neg x) = Pos x + +instance Negable Bool where + not = P.not + +instance Monoid m => Negable (Maybe m) where + not (Just _) = Nothing + not Nothing = Just mempty + +instance (Negable a, Negable b) => Negable (a, b) where + not (x, y) = (not x, not y) + +instance (Negable a, Negable b) => Negable (Either a b) where + not (Left x) = Left $ not x + not (Right y) = Right $ not y diff --git a/src/Data/Algebra/Boolean/NormalForm.hs b/src/Data/Algebra/Boolean/NormalForm.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algebra/Boolean/NormalForm.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Oleg Grenrus 2014 +-- License : MIT +-- Maintainer: Oleg Grenrus +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Data.Algebra.Boolean.NormalForm ( + NormalForm(..), + module Data.Algebra.Boolean.CoBoolean + ) where + +import Data.Algebra.Boolean.CoBoolean +import Data.Algebra.Boolean.FreeBoolean + +import GHC.Exts (Constraint) + +-- | Class unifying different boolean normal forms. +class CoBoolean1 nf => NormalForm nf where + -- | 'NormalForm' could be constrained, so the 'Set' based implementations could be included. + type NFConstraint nf a :: Constraint + type NFConstraint nf a = () + + -- | Lift a value into normal form. + toNormalForm :: a -> nf a + + -- | Simplify the formula, if some terms are ⊥ or ⊤. + simplify :: (NFConstraint nf a) => (a -> Maybe Bool) -> nf a -> nf a + + -- | transform from free boolean form + fromFreeBoolean :: (NFConstraint nf a) => FreeBoolean a -> nf a + +instance NormalForm FreeBoolean where + toNormalForm = FBValue + simplify _ = id + fromFreeBoolean = id diff --git a/tests/BooleanLaws.hs b/tests/BooleanLaws.hs new file mode 100644 --- /dev/null +++ b/tests/BooleanLaws.hs @@ -0,0 +1,91 @@ +module BooleanLaws (monotoneLaws, nonMonotoneLaws) where + +import Test.Tasty +import Test.Tasty.QuickCheck as QC + +import Prelude hiding ((||),(&&),not) +import Data.Algebra.Boolean + +associativityOrProp :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool +associativityOrProp eq x y z = (x || (y || z)) `eq` ((x || y) || z) + +associativityAndProp :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool +associativityAndProp eq x y z = (x || (y || z)) `eq` ((x || y) || z) + +commutativeOrProp :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool +commutativeOrProp eq x y = (x || y) `eq` (y || x) + +commutativeAndProp :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool +commutativeAndProp eq x y = (x && y) `eq` (y && x) + +distributivity1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool +distributivity1Prop eq x y z = (x && (y || z)) `eq` ((x && y) || (x && z)) + +distributivity2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool +distributivity2Prop eq x y z = (x || (y && z)) `eq` ((x || y) && (x || z)) + +identityOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +identityOrProp eq x = (x || false) `eq` x + +identityAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +identityAndProp eq x = (x && true) `eq` x + +annihilatorOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +annihilatorOrProp eq x = (x || true) `eq` true + +annihilatorAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +annihilatorAndProp eq x = (x && false) `eq` false + +idempotenceOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +idempotenceOrProp eq x = (x || x) `eq` x + +idempotenceAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +idempotenceAndProp eq x = (x && x) `eq` x + +absorption1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool +absorption1Prop eq x y = (x && (x || y)) `eq` x + +absorption2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool +absorption2Prop eq x y = (x || (x && y)) `eq` x + +complementationOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +complementationOrProp eq x = (x || not x) `eq` true + +complementationAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +complementationAndProp eq x = (x && not x) `eq` false + +doubleNegationProp :: Boolean a => (a -> a -> Bool) -> a -> Bool +doubleNegationProp eq x = not (not x) `eq` x + +deMorgan1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool +deMorgan1Prop eq x y = (not x && not y) `eq` not (x || y) + +deMorgan2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool +deMorgan2Prop eq x y = (not x || not y) `eq` not (x && y) + +monotoneLaws :: (Arbitrary a, Show a, Boolean a) => (a -> a -> Bool) -> TestTree +monotoneLaws eq = testGroup "Monotone boolean laws" + [ QC.testProperty "associativity or" $ associativityOrProp eq + , QC.testProperty "associativity and" $ associativityAndProp eq + , QC.testProperty "commutativity or" $ commutativeOrProp eq + , QC.testProperty "commutativity and" $ commutativeAndProp eq + , QC.testProperty "distributivity 1" $ distributivity1Prop eq + , QC.testProperty "distributivity 2" $ distributivity2Prop eq + , QC.testProperty "identity or" $ identityOrProp eq + , QC.testProperty "identity and" $ identityAndProp eq + , QC.testProperty "annihilator or" $ annihilatorOrProp eq + , QC.testProperty "annihilator and" $ annihilatorAndProp eq + , QC.testProperty "idempotence or" $ idempotenceOrProp eq + , QC.testProperty "idempotence and" $ idempotenceAndProp eq + , QC.testProperty "absorption 1" $ absorption1Prop eq + , QC.testProperty "absorption 2" $ absorption2Prop eq + ] + +nonMonotoneLaws :: (Arbitrary a, Show a, Boolean a) => (a -> a -> Bool) -> TestTree +nonMonotoneLaws eq = testGroup "Non monotone boolean laws" + [ QC.testProperty "complementation or" $ complementationOrProp eq + , QC.testProperty "complementation and" $ complementationAndProp eq + , QC.testProperty "double negation" $ doubleNegationProp eq + , QC.testProperty "de Morgan 1" $ deMorgan1Prop eq + , QC.testProperty "de Morgan 2" $ deMorgan2Prop eq + ] diff --git a/tests/CNFList.hs b/tests/CNFList.hs new file mode 100644 --- /dev/null +++ b/tests/CNFList.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module CNFList (tests) where + +import BooleanLaws +import SimplifyLaws +import BooleanModelLaws + +import FreeBoolean + +import Test.Tasty +import Test.QuickCheck + +import Control.Applicative +import Data.Function (on) + +import Data.Algebra.Boolean.Negable (Negable, Neg(..)) +import Data.Algebra.Boolean.CNF.List + +instance Arbitrary a => Arbitrary (Neg a) where + arbitrary = oneof [ Pos <$> arbitrary, Pos <$> arbitrary ] + +instance (Negable a, Arbitrary a) => Arbitrary (CNF a) where + arbitrary = fromFreeBoolean <$> arbitrary + +tests :: TestTree +tests = testGroup "CNF list implementation" + [ monotoneLaws eq + , simplifyLaws (undefined :: CNF (Either Bool Bool)) + , booleanModelLaws (undefined :: CNF (Either Bool Bool)) + ] + +eq :: CNF (Neg Int) -> CNF (Neg Int) -> Bool +eq = (==) `on` toBool diff --git a/tests/CNFSet.hs b/tests/CNFSet.hs new file mode 100644 --- /dev/null +++ b/tests/CNFSet.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module CNFSet (tests) where + +import BooleanLaws +import NegableLaws +import SimplifyLaws +import BooleanModelLaws + +import FreeBoolean + +import Test.Tasty +import Test.QuickCheck + +import Control.Applicative +import Data.Monoid +import Data.Function (on) + +import Data.Algebra.Boolean.Negable (Negable) +import Data.Algebra.Boolean.CNF.Set + +instance Arbitrary a => Arbitrary (Sum a) where + arbitrary = Sum <$> arbitrary + +instance (Ord a, Negable a, Arbitrary a) => Arbitrary (CNF a) where + arbitrary = fromFreeBoolean <$> arbitrary + +tests :: TestTree +tests = testGroup "CNF set implementation" + [ monotoneLaws eq + , nonMonotoneLaws eq + , negableLaws eq + , simplifyLaws (undefined :: CNF (Either Bool Bool)) + , booleanModelLaws (undefined :: CNF (Either Bool Bool)) + ] + +eq :: CNF (Maybe (Sum Int)) -> CNF (Maybe (Sum Int)) -> Bool +eq = (==) `on` toBool diff --git a/tests/DNFList.hs b/tests/DNFList.hs new file mode 100644 --- /dev/null +++ b/tests/DNFList.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module DNFList (tests) where + +import BooleanLaws +import SimplifyLaws +import BooleanModelLaws + +import FreeBoolean + +import Test.Tasty +import Test.QuickCheck + +import Control.Applicative +import Data.Function (on) + +import Data.Algebra.Boolean.Negable (Negable, Neg(..)) +import Data.Algebra.Boolean.DNF.List + +instance Arbitrary a => Arbitrary (Neg a) where + arbitrary = oneof [ Pos <$> arbitrary, Pos <$> arbitrary ] + +instance (Negable a, Arbitrary a) => Arbitrary (DNF a) where + arbitrary = fromFreeBoolean <$> arbitrary + +tests :: TestTree +tests = testGroup "DNF list implementation" + [ monotoneLaws eq + , simplifyLaws (undefined :: DNF (Either Bool Bool)) + , booleanModelLaws (undefined :: DNF (Either Bool Bool)) + ] + +eq :: DNF (Neg Int) -> DNF (Neg Int) -> Bool +eq = (==) `on` toBool diff --git a/tests/DNFSet.hs b/tests/DNFSet.hs new file mode 100644 --- /dev/null +++ b/tests/DNFSet.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module DNFSet (tests) where + +import BooleanLaws +import NegableLaws +import SimplifyLaws +import BooleanModelLaws + +import FreeBoolean + +import Test.Tasty +import Test.QuickCheck + +import Control.Applicative +import Data.Monoid +import Data.Function (on) + +import Data.Algebra.Boolean.Negable (Negable) +import Data.Algebra.Boolean.DNF.Set + +instance Arbitrary a => Arbitrary (Sum a) where + arbitrary = Sum <$> arbitrary + +instance (Ord a, Negable a, Arbitrary a) => Arbitrary (DNF a) where + arbitrary = fromFreeBoolean <$> arbitrary + +tests :: TestTree +tests = testGroup "DNF set implementation" + [ monotoneLaws eq + , nonMonotoneLaws eq + , negableLaws eq + , simplifyLaws (undefined :: DNF (Either Bool Bool)) + , booleanModelLaws (undefined :: DNF (Either Bool Bool)) + ] + +eq :: DNF (Maybe (Sum Int)) -> DNF (Maybe (Sum Int)) -> Bool +eq = (==) `on` toBool diff --git a/tests/FreeBoolean.hs b/tests/FreeBoolean.hs new file mode 100644 --- /dev/null +++ b/tests/FreeBoolean.hs @@ -0,0 +1,33 @@ +module FreeBoolean ( + freeBooleanHeight, + module Data.Algebra.Boolean.FreeBoolean + ) where + +import Test.Tasty.QuickCheck + +import Control.Applicative + +import Data.Algebra.Boolean.FreeBoolean + +instance Arbitrary a => Arbitrary (FreeBoolean a) where + arbitrary = sized arbitrary' + where arbitrary' 0 = frequency [ + (10, FBValue <$> arbitrary), + (1, pure FBTrue), + (1, pure FBFalse) + ] + arbitrary' n = oneof [ + FBValue <$> arbitrary, + FBNot <$> arbitrary'', + FBAnd <$> arbitrary'' <*> arbitrary'', + FBOr <$> arbitrary'' <*> arbitrary'' + ] + where arbitrary'' = arbitrary' $ n `div` 2 + +freeBooleanHeight :: FreeBoolean a -> Int +freeBooleanHeight FBTrue = 0 +freeBooleanHeight FBFalse = 0 +freeBooleanHeight (FBValue _) = 0 +freeBooleanHeight (FBNot x) = 1 + freeBooleanHeight x +freeBooleanHeight (FBAnd a b) = 1 + max (freeBooleanHeight a) (freeBooleanHeight b) +freeBooleanHeight (FBOr a b) = 1 + max (freeBooleanHeight a) (freeBooleanHeight b) diff --git a/tests/FreeBooleanTests.hs b/tests/FreeBooleanTests.hs new file mode 100644 --- /dev/null +++ b/tests/FreeBooleanTests.hs @@ -0,0 +1,24 @@ +module FreeBooleanTests where + +import BooleanLaws +import NegableLaws +import SimplifyLaws +import BooleanModelLaws + +import FreeBoolean + +import Data.Function (on) + +import Test.Tasty + +tests :: TestTree +tests = testGroup "Free boolean" + [ monotoneLaws eq + , nonMonotoneLaws eq + , negableLaws eq + , simplifyLaws (undefined :: FreeBoolean (Either Bool Bool)) + , booleanModelLaws (undefined :: FreeBoolean (Either Bool Bool)) + ] + +eq :: FreeBoolean Int -> FreeBoolean Int -> Bool +eq = (==) `on` toBoolWith (1==) diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,25 @@ +module Main (main) where + +import qualified NNFTree +import qualified NNFSet +import qualified DNFList +import qualified DNFSet +import qualified CNFList +import qualified CNFSet +import qualified FreeBooleanTests as FBT + +import Test.Tasty + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = testGroup "Tests" [ + NNFTree.tests, + NNFSet.tests, + CNFList.tests, + CNFSet.tests, + DNFList.tests, + DNFSet.tests, + FBT.tests + ] diff --git a/tests/NNFSet.hs b/tests/NNFSet.hs new file mode 100644 --- /dev/null +++ b/tests/NNFSet.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module NNFSet (tests) where + +import BooleanLaws +import NegableLaws +import SimplifyLaws +import BooleanModelLaws + +import FreeBoolean + +import Test.Tasty +import Test.QuickCheck + +import Control.Applicative +import Data.Monoid +import Data.Function (on) + +import Data.Algebra.Boolean.Negable (Negable) +import Data.Algebra.Boolean.NNF.Set + +instance Arbitrary a => Arbitrary (Sum a) where + arbitrary = Sum <$> arbitrary + +instance (Ord a, Negable a, Arbitrary a) => Arbitrary (NNF a) where + arbitrary = fromFreeBoolean <$> arbitrary + +tests :: TestTree +tests = testGroup "NNF set implementation" + [ monotoneLaws eq + , nonMonotoneLaws eq + , negableLaws eq + , simplifyLaws (undefined :: NNF (Either Bool Bool)) + , booleanModelLaws (undefined :: NNF (Either Bool Bool)) + ] + +eq :: NNF (Maybe (Sum Int)) -> NNF (Maybe (Sum Int)) -> Bool +eq = (==) `on` toBool diff --git a/tests/NNFTree.hs b/tests/NNFTree.hs new file mode 100644 --- /dev/null +++ b/tests/NNFTree.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module NNFTree (tests) where + +import BooleanLaws +import NegableLaws +import SimplifyLaws +import BooleanModelLaws + +import FreeBoolean + +import Test.Tasty +import Test.QuickCheck + +import Control.Applicative +import Data.Function (on) + +import Data.Algebra.Boolean.Negable (Negable) +import Data.Algebra.Boolean.NNF.Tree + +instance (Negable a, Arbitrary a) => Arbitrary (NNF a) where + arbitrary = fromFreeBoolean <$> arbitrary + +tests :: TestTree +tests = testGroup "NNF tree implementation" + [ monotoneLaws eq + , nonMonotoneLaws eq + , negableLaws eq + , simplifyLaws (undefined :: NNF (Either Bool Bool)) + , booleanModelLaws (undefined :: NNF (Either Bool Bool)) + ] + +eq :: NNF Bool -> NNF Bool -> Bool +eq = (==) `on` toBool diff --git a/tests/NegableLaws.hs b/tests/NegableLaws.hs new file mode 100644 --- /dev/null +++ b/tests/NegableLaws.hs @@ -0,0 +1,15 @@ +module NegableLaws (negableLaws) where + +import Test.Tasty +import Test.Tasty.QuickCheck as QC + +import Prelude hiding (not) +import Data.Algebra.Boolean.Negable + +doubleNegationProp :: Negable a => (a -> a -> Bool) -> a -> Bool +doubleNegationProp eq x = not (not x) `eq` x + +negableLaws :: (Arbitrary a, Show a, Negable a) => (a -> a -> Bool) -> TestTree +negableLaws eq = testGroup "Negable laws" + [ QC.testProperty "double negation" $ doubleNegationProp eq + ] diff --git a/tests/SimplifyLaws.hs b/tests/SimplifyLaws.hs new file mode 100644 --- /dev/null +++ b/tests/SimplifyLaws.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ConstraintKinds #-} +module SimplifyLaws (simplifyLaws) where + +import Test.Tasty +import Test.Tasty.QuickCheck as QC + +import Data.Algebra.Boolean.CoBoolean +import Data.Algebra.Boolean.NormalForm + +simplifyProperty :: (CoBoolean a, NormalForm nf, NFConstraint nf (Either a Bool)) => nf (Either a Bool) -> Bool +simplifyProperty nf = toBooleanWith toBoolean (simplify f nf) == (toBooleanWith toBoolean nf :: Bool) + where f (Right b) = Just b + f (Left _) = Nothing + +simplifyLaws :: forall a nf. (CoBoolean a, NormalForm nf, NFConstraint nf (Either a Bool), Show (nf (Either a Bool)), Arbitrary (nf (Either a Bool))) => nf (Either a Bool) -> TestTree +simplifyLaws _ = QC.testProperty "simplify property" prop + where prop :: nf (Either a Bool) -> Bool + prop = simplifyProperty