msakai / toysolver / 496

Committed 10 Nov 2024 11:05AM UTC coverage: 69.994% (-1.1%) from 71.113%

Build # 496

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #117 from msakai/update-coveralls-and-haddock

GitHub Actions: Update coveralls and haddock configuration

Run Details

9872 of 14104 relevant lines covered (69.99%)

0.7 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

46.99

/src/ToySolver/Data/BoolExpr.hs

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.BoolExpr
-- Copyright   :  (c) Masahiro Sakai 2014-2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Boolean expression over a given type of atoms
--
-----------------------------------------------------------------------------
module ToySolver.Data.BoolExpr
  (
  -- * BoolExpr type
    BoolExpr (..)

  -- * Operations
  , fold
  , simplify
  ) where

import Control.DeepSeq
import Control.Monad
import Data.Data
import Data.Hashable
import Data.Traversable
import ToySolver.Data.Boolean
import ToySolver.Data.IntVar

-- | Boolean expression over a given type of atoms
data BoolExpr a
  = Atom a
  | And [BoolExpr a]
  | Or [BoolExpr a]
  | Not (BoolExpr a)
  | Imply (BoolExpr a) (BoolExpr a)
  | Equiv (BoolExpr a) (BoolExpr a)
  | ITE (BoolExpr a) (BoolExpr a) (BoolExpr a)
  deriving (Eq, Ord, Show, Read, Typeable, Data)

instance Functor BoolExpr where
  fmap = fmapDefault

instance Applicative BoolExpr where
  pure = Atom
  (<*>) = ap

instance Monad BoolExpr where
  return = pure
  m >>= f = fold f m

instance Foldable BoolExpr where
  foldMap = foldMapDefault

instance Traversable BoolExpr where
  traverse f (Atom x) = Atom <$> f x
  traverse f (And xs) = And <$> sequenceA (fmap (traverse f) xs)
  traverse f (Or xs) = Or <$> sequenceA (fmap (traverse f) xs)
  traverse f (Not x) = Not <$> traverse f x
  traverse f (Imply x y) = Imply <$> traverse f x <*> traverse f y
  traverse f (Equiv x y) = Equiv <$> traverse f x <*> traverse f y
  traverse f (ITE c t e) = ITE <$> traverse f c <*> traverse f t <*> traverse f e

instance NFData a => NFData (BoolExpr a) where
  rnf (Atom a) = rnf a
  rnf (And xs) = rnf xs
  rnf (Or xs) = rnf xs
  rnf (Not x) = rnf x
  rnf (Imply x y) = rnf x `seq` rnf y
  rnf (Equiv x y) = rnf x `seq` rnf y
  rnf (ITE c t e) = rnf c `seq` rnf t `seq` rnf e

instance Hashable a => Hashable (BoolExpr a) where
  hashWithSalt s (Atom a) = s `hashWithSalt` (0::Int) `hashWithSalt` a
  hashWithSalt s (And xs) = s `hashWithSalt` (1::Int) `hashWithSalt` xs
  hashWithSalt s (Or xs)  = s `hashWithSalt` (2::Int) `hashWithSalt` xs
  hashWithSalt s (Not x)  = s `hashWithSalt` (3::Int) `hashWithSalt` x
  hashWithSalt s (Imply x y) = s `hashWithSalt` (4::Int) `hashWithSalt` x `hashWithSalt` y
  hashWithSalt s (Equiv x y) = s `hashWithSalt` (5::Int) `hashWithSalt` x `hashWithSalt` y
  hashWithSalt s (ITE c t e) = s `hashWithSalt` (6::Int) `hashWithSalt` c `hashWithSalt` t `hashWithSalt` e

instance Complement (BoolExpr a) where
  notB = Not

instance MonotoneBoolean (BoolExpr a) where
  andB = And
  orB  = Or

instance IfThenElse (BoolExpr a) (BoolExpr a) where
  ite = ITE

instance Boolean (BoolExpr a) where
  (.=>.) = Imply
  (.<=>.) = Equiv

instance Variables a => Variables (BoolExpr a) where
  vars = foldMap vars


fold :: Boolean b => (atom -> b) -> BoolExpr atom -> b
fold f = g
  where
    g (Atom a) = f a
    g (Or xs) = orB (map g xs)
    g (And xs) = andB (map g xs)
    g (Not x) = notB (g x)
    g (Imply x y) = g x .=>. g y
    g (Equiv x y) = g x .<=>. g y
    g (ITE c t e) = ite (g c) (g t) (g e)

{-# RULES
  "fold/fmap"    forall f g e.  fold f (fmap g e) = fold (f.g) e
 #-}

instance Eval m a Bool => Eval m (BoolExpr a) Bool where
  eval m = fold (eval m)

simplify :: BoolExpr a -> BoolExpr a
simplify = runSimplify . fold (Simplify . Atom)

newtype Simplify a = Simplify{ runSimplify :: BoolExpr a }

instance Complement (Simplify a) where
  notB (Simplify (Not x)) = Simplify x
  notB (Simplify x) = Simplify (Not x)

instance MonotoneBoolean (Simplify a) where
  orB xs
    | any isTrue ys = Simplify true
    | otherwise = Simplify $ Or ys
    where
      ys = concat [f x | Simplify x <- xs]
      f (Or zs) = zs
      f z = [z]
  andB xs
    | any isFalse ys = Simplify false
    | otherwise = Simplify $ And ys
    where
      ys = concat [f x | Simplify x <- xs]
      f (And zs) = zs
      f z = [z]

instance IfThenElse (Simplify a) (Simplify a) where
  ite (Simplify c) (Simplify t) (Simplify e)
    | isTrue c  = Simplify t
    | isFalse c = Simplify e
    | otherwise = Simplify (ITE c t e)

instance Boolean (Simplify a) where
  Simplify x .=>. Simplify y
    | isFalse x = true
    | isTrue y  = true
    | isTrue x  = Simplify y
    | isFalse y = notB (Simplify x)
    | otherwise = Simplify (x .=>. y)

isTrue :: BoolExpr a -> Bool
isTrue (And []) = True
isTrue _ = False

isFalse :: BoolExpr a -> Bool
isFalse (Or []) = True
isFalse _ = False

1	{-# LANGUAGE DeriveDataTypeable #-}
2	{-# LANGUAGE FlexibleContexts #-}
3	{-# LANGUAGE FlexibleInstances #-}
4	{-# LANGUAGE MultiParamTypeClasses #-}
5	{-# OPTIONS_GHC -Wall #-}
6	{-# OPTIONS_HADDOCK show-extensions #-}
7	-----------------------------------------------------------------------------
8	-- \|
9	-- Module : ToySolver.Data.BoolExpr
10	-- Copyright : (c) Masahiro Sakai 2014-2015
11	-- License : BSD-style
12	--
13	-- Maintainer : masahiro.sakai@gmail.com
14	-- Stability : provisional
15	-- Portability : non-portable
16	--
17	-- Boolean expression over a given type of atoms
18	--
19	-----------------------------------------------------------------------------
20	module ToySolver.Data.BoolExpr
21	(
22	-- * BoolExpr type
23	BoolExpr (..)
24
25	-- * Operations
26	, fold
27	, simplify
28	) where
29
30	import Control.DeepSeq
31	import Control.Monad
32	import Data.Data
33	import Data.Hashable
34	import Data.Traversable
35	import ToySolver.Data.Boolean
36	import ToySolver.Data.IntVar
37
38	-- \| Boolean expression over a given type of atoms
39	data BoolExpr a
40	= Atom a
41	\| And [BoolExpr a]
42	\| Or [BoolExpr a]
43	\| Not (BoolExpr a)
44	\| Imply (BoolExpr a) (BoolExpr a)
45	\| Equiv (BoolExpr a) (BoolExpr a)
46	\| ITE (BoolExpr a) (BoolExpr a) (BoolExpr a)
47	deriving (Eq, Ord, Show, Read, Typeable, Data)	×
48
49	instance Functor BoolExpr where	×
50	fmap = fmapDefault	1✔
51
52	instance Applicative BoolExpr where	×
53	pure = Atom	1✔
54	(<*>) = ap	1✔
55
56	instance Monad BoolExpr where	×
57	return = pure	1✔
58	m >>= f = fold f m	1✔
59
60	instance Foldable BoolExpr where	×
61	foldMap = foldMapDefault	1✔
62
63	instance Traversable BoolExpr where	×
64	traverse f (Atom x) = Atom <$> f x	1✔
65	traverse f (And xs) = And <$> sequenceA (fmap (traverse f) xs)	1✔
66	traverse f (Or xs) = Or <$> sequenceA (fmap (traverse f) xs)	1✔
67	traverse f (Not x) = Not <$> traverse f x	1✔
68	traverse f (Imply x y) = Imply <$> traverse f x <*> traverse f y	1✔
69	traverse f (Equiv x y) = Equiv <$> traverse f x <*> traverse f y	1✔
70	traverse f (ITE c t e) = ITE <$> traverse f c <> traverse f t <> traverse f e	1✔
71
72	instance NFData a => NFData (BoolExpr a) where
73	rnf (Atom a) = rnf a	×
74	rnf (And xs) = rnf xs	×
75	rnf (Or xs) = rnf xs	×
76	rnf (Not x) = rnf x	×
77	rnf (Imply x y) = rnf x `seq` rnf y	×
78	rnf (Equiv x y) = rnf x `seq` rnf y	×
79	rnf (ITE c t e) = rnf c `seq` rnf t `seq` rnf e	×
80
81	instance Hashable a => Hashable (BoolExpr a) where	×
82	hashWithSalt s (Atom a) = s `hashWithSalt` (0::Int) `hashWithSalt` a	×
83	hashWithSalt s (And xs) = s `hashWithSalt` (1::Int) `hashWithSalt` xs	×
84	hashWithSalt s (Or xs) = s `hashWithSalt` (2::Int) `hashWithSalt` xs	×
85	hashWithSalt s (Not x) = s `hashWithSalt` (3::Int) `hashWithSalt` x	×
86	hashWithSalt s (Imply x y) = s `hashWithSalt` (4::Int) `hashWithSalt` x `hashWithSalt` y	×
87	hashWithSalt s (Equiv x y) = s `hashWithSalt` (5::Int) `hashWithSalt` x `hashWithSalt` y	×
88	hashWithSalt s (ITE c t e) = s `hashWithSalt` (6::Int) `hashWithSalt` c `hashWithSalt` t `hashWithSalt` e	×
89
90	instance Complement (BoolExpr a) where
91	notB = Not	1✔
92
93	instance MonotoneBoolean (BoolExpr a) where	1✔
94	andB = And	1✔
95	orB = Or	1✔
96
97	instance IfThenElse (BoolExpr a) (BoolExpr a) where
98	ite = ITE	1✔
99
100	instance Boolean (BoolExpr a) where
101	(.=>.) = Imply	1✔
102	(.<=>.) = Equiv	1✔
103
104	instance Variables a => Variables (BoolExpr a) where
105	vars = foldMap vars	×
106
107
108	fold :: Boolean b => (atom -> b) -> BoolExpr atom -> b
109	fold f = g	1✔
110	where
111	g (Atom a) = f a	1✔
112	g (Or xs) = orB (map g xs)	1✔
113	g (And xs) = andB (map g xs)	1✔
114	g (Not x) = notB (g x)	1✔
115	g (Imply x y) = g x .=>. g y	1✔
116	g (Equiv x y) = g x .<=>. g y	1✔
117	g (ITE c t e) = ite (g c) (g t) (g e)	1✔
118
119	{-# RULES
120	"fold/fmap" forall f g e. fold f (fmap g e) = fold (f.g) e
121	#-}
122
123	instance Eval m a Bool => Eval m (BoolExpr a) Bool where
124	eval m = fold (eval m)	1✔
125
126	simplify :: BoolExpr a -> BoolExpr a
127	simplify = runSimplify . fold (Simplify . Atom)	1✔
128
129	newtype Simplify a = Simplify{ runSimplify :: BoolExpr a }	1✔
130
131	instance Complement (Simplify a) where
132	notB (Simplify (Not x)) = Simplify x	×
133	notB (Simplify x) = Simplify (Not x)	×
134
135	instance MonotoneBoolean (Simplify a) where	×
136	orB xs	1✔
137	\| any isTrue ys = Simplify true	×
138	\| otherwise = Simplify $ Or ys	×
139	where
140	ys = concat [f x \| Simplify x <- xs]	×
141	f (Or zs) = zs	×
142	f z = [z]	×
143	andB xs	1✔
144	\| any isFalse ys = Simplify false	1✔
145	\| otherwise = Simplify $ And ys	×
146	where
147	ys = concat [f x \| Simplify x <- xs]	1✔
148	f (And zs) = zs	1✔
149	f z = [z]	1✔
150
151	instance IfThenElse (Simplify a) (Simplify a) where
152	ite (Simplify c) (Simplify t) (Simplify e)	×
153	\| isTrue c = Simplify t	×
154	\| isFalse c = Simplify e	×
155	\| otherwise = Simplify (ITE c t e)	×
156
157	instance Boolean (Simplify a) where	×
158	Simplify x .=>. Simplify y	×
159	\| isFalse x = true	×
160	\| isTrue y = true	×
161	\| isTrue x = Simplify y	×
162	\| isFalse y = notB (Simplify x)	×
163	\| otherwise = Simplify (x .=>. y)	×
164
165	isTrue :: BoolExpr a -> Bool
166	isTrue (And []) = True	×
167	isTrue _ = False	×
168
169	isFalse :: BoolExpr a -> Bool
170	isFalse (Or []) = True	1✔
171	isFalse _ = False	1✔

msakai / toysolver / 496

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous