{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : Data.Diagram.Simple
-- Copyright   : (c) Eddie Jones 2020
-- License     : BSD-3
-- Maintainer  : eddiejones2108@gmail.com
-- Stability   : experimental
--
-- Reduced Ordered Binary Decision Diagrams
module Data.Diagram.Simple
  ( -- * Diagram
    Diagram,
    runDiagram,

    -- * Propositions
    Prop,
    mkProp,
    true,
    false,
    atom,
    notAtom,
    mapAtom,
    bindAtom,

    -- * Combinations
    Data.Diagram.Simple.and,
    Data.Diagram.Simple.or,
    Data.Diagram.Simple.not,
    restrict,

    -- * Summary
    fold,
    anySat,
  )
where

import Control.Monad.State
import qualified Data.Diagram as D
import Data.Functor.Classes
import Data.Functor.Identity
import Data.Hashable
import Data.Hashable.Lifted
import qualified Data.Map as M

data Memo l s
  = And (Prop l s) (Prop l s)
  | Or (Prop l s) (Prop l s)
  | Not (Prop l s)
  | Restr l Bool (Prop l s)
  deriving (Memo l s -> Memo l s -> Bool
(Memo l s -> Memo l s -> Bool)
-> (Memo l s -> Memo l s -> Bool) -> Eq (Memo l s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall l s. Eq l => Memo l s -> Memo l s -> Bool
/= :: Memo l s -> Memo l s -> Bool
$c/= :: forall l s. Eq l => Memo l s -> Memo l s -> Bool
== :: Memo l s -> Memo l s -> Bool
$c== :: forall l s. Eq l => Memo l s -> Memo l s -> Bool
Eq, Eq (Memo l s)
Eq (Memo l s) =>
(Memo l s -> Memo l s -> Ordering)
-> (Memo l s -> Memo l s -> Bool)
-> (Memo l s -> Memo l s -> Bool)
-> (Memo l s -> Memo l s -> Bool)
-> (Memo l s -> Memo l s -> Bool)
-> (Memo l s -> Memo l s -> Memo l s)
-> (Memo l s -> Memo l s -> Memo l s)
-> Ord (Memo l s)
Memo l s -> Memo l s -> Bool
Memo l s -> Memo l s -> Ordering
Memo l s -> Memo l s -> Memo l s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall l s. Ord l => Eq (Memo l s)
forall l s. Ord l => Memo l s -> Memo l s -> Bool
forall l s. Ord l => Memo l s -> Memo l s -> Ordering
forall l s. Ord l => Memo l s -> Memo l s -> Memo l s
min :: Memo l s -> Memo l s -> Memo l s
$cmin :: forall l s. Ord l => Memo l s -> Memo l s -> Memo l s
max :: Memo l s -> Memo l s -> Memo l s
$cmax :: forall l s. Ord l => Memo l s -> Memo l s -> Memo l s
>= :: Memo l s -> Memo l s -> Bool
$c>= :: forall l s. Ord l => Memo l s -> Memo l s -> Bool
> :: Memo l s -> Memo l s -> Bool
$c> :: forall l s. Ord l => Memo l s -> Memo l s -> Bool
<= :: Memo l s -> Memo l s -> Bool
$c<= :: forall l s. Ord l => Memo l s -> Memo l s -> Bool
< :: Memo l s -> Memo l s -> Bool
$c< :: forall l s. Ord l => Memo l s -> Memo l s -> Bool
compare :: Memo l s -> Memo l s -> Ordering
$ccompare :: forall l s. Ord l => Memo l s -> Memo l s -> Ordering
$cp1Ord :: forall l s. Ord l => Eq (Memo l s)
Ord)

-- | A binary decision diagram
newtype Diagram l s a = Diagram
  { Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag :: D.Diagram (Node l) Bool s (State (M.Map (Memo l s) (Prop l s))) a
  }
  deriving (a -> Diagram l s b -> Diagram l s a
(a -> b) -> Diagram l s a -> Diagram l s b
(forall a b. (a -> b) -> Diagram l s a -> Diagram l s b)
-> (forall a b. a -> Diagram l s b -> Diagram l s a)
-> Functor (Diagram l s)
forall a b. a -> Diagram l s b -> Diagram l s a
forall a b. (a -> b) -> Diagram l s a -> Diagram l s b
forall l s a b. a -> Diagram l s b -> Diagram l s a
forall l s a b. (a -> b) -> Diagram l s a -> Diagram l s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Diagram l s b -> Diagram l s a
$c<$ :: forall l s a b. a -> Diagram l s b -> Diagram l s a
fmap :: (a -> b) -> Diagram l s a -> Diagram l s b
$cfmap :: forall l s a b. (a -> b) -> Diagram l s a -> Diagram l s b
Functor, Functor (Diagram l s)
a -> Diagram l s a
Functor (Diagram l s) =>
(forall a. a -> Diagram l s a)
-> (forall a b.
    Diagram l s (a -> b) -> Diagram l s a -> Diagram l s b)
-> (forall a b c.
    (a -> b -> c) -> Diagram l s a -> Diagram l s b -> Diagram l s c)
-> (forall a b. Diagram l s a -> Diagram l s b -> Diagram l s b)
-> (forall a b. Diagram l s a -> Diagram l s b -> Diagram l s a)
-> Applicative (Diagram l s)
Diagram l s a -> Diagram l s b -> Diagram l s b
Diagram l s a -> Diagram l s b -> Diagram l s a
Diagram l s (a -> b) -> Diagram l s a -> Diagram l s b
(a -> b -> c) -> Diagram l s a -> Diagram l s b -> Diagram l s c
forall a. a -> Diagram l s a
forall l s. Functor (Diagram l s)
forall a b. Diagram l s a -> Diagram l s b -> Diagram l s a
forall a b. Diagram l s a -> Diagram l s b -> Diagram l s b
forall a b. Diagram l s (a -> b) -> Diagram l s a -> Diagram l s b
forall l s a. a -> Diagram l s a
forall a b c.
(a -> b -> c) -> Diagram l s a -> Diagram l s b -> Diagram l s c
forall l s a b. Diagram l s a -> Diagram l s b -> Diagram l s a
forall l s a b. Diagram l s a -> Diagram l s b -> Diagram l s b
forall l s a b.
Diagram l s (a -> b) -> Diagram l s a -> Diagram l s b
forall l s a b c.
(a -> b -> c) -> Diagram l s a -> Diagram l s b -> Diagram l s c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Diagram l s a -> Diagram l s b -> Diagram l s a
$c<* :: forall l s a b. Diagram l s a -> Diagram l s b -> Diagram l s a
*> :: Diagram l s a -> Diagram l s b -> Diagram l s b
$c*> :: forall l s a b. Diagram l s a -> Diagram l s b -> Diagram l s b
liftA2 :: (a -> b -> c) -> Diagram l s a -> Diagram l s b -> Diagram l s c
$cliftA2 :: forall l s a b c.
(a -> b -> c) -> Diagram l s a -> Diagram l s b -> Diagram l s c
<*> :: Diagram l s (a -> b) -> Diagram l s a -> Diagram l s b
$c<*> :: forall l s a b.
Diagram l s (a -> b) -> Diagram l s a -> Diagram l s b
pure :: a -> Diagram l s a
$cpure :: forall l s a. a -> Diagram l s a
$cp1Applicative :: forall l s. Functor (Diagram l s)
Applicative, Applicative (Diagram l s)
a -> Diagram l s a
Applicative (Diagram l s) =>
(forall a b.
 Diagram l s a -> (a -> Diagram l s b) -> Diagram l s b)
-> (forall a b. Diagram l s a -> Diagram l s b -> Diagram l s b)
-> (forall a. a -> Diagram l s a)
-> Monad (Diagram l s)
Diagram l s a -> (a -> Diagram l s b) -> Diagram l s b
Diagram l s a -> Diagram l s b -> Diagram l s b
forall a. a -> Diagram l s a
forall l s. Applicative (Diagram l s)
forall a b. Diagram l s a -> Diagram l s b -> Diagram l s b
forall a b. Diagram l s a -> (a -> Diagram l s b) -> Diagram l s b
forall l s a. a -> Diagram l s a
forall l s a b. Diagram l s a -> Diagram l s b -> Diagram l s b
forall l s a b.
Diagram l s a -> (a -> Diagram l s b) -> Diagram l s b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Diagram l s a
$creturn :: forall l s a. a -> Diagram l s a
>> :: Diagram l s a -> Diagram l s b -> Diagram l s b
$c>> :: forall l s a b. Diagram l s a -> Diagram l s b -> Diagram l s b
>>= :: Diagram l s a -> (a -> Diagram l s b) -> Diagram l s b
$c>>= :: forall l s a b.
Diagram l s a -> (a -> Diagram l s b) -> Diagram l s b
$cp1Monad :: forall l s. Applicative (Diagram l s)
Monad)

-- | Extract non-diagrammatic information
runDiagram :: (forall s. Diagram l s a) -> a
runDiagram :: (forall s. Diagram l s a) -> a
runDiagram d :: forall s. Diagram l s a
d = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ (forall s. Diagram (Node l) Bool s Identity a) -> Identity a
forall (m :: * -> *) (f :: * -> *) a b.
Monad m =>
(forall s. Diagram f a s m b) -> m b
D.runDiagram ((State (Map (Memo l s) (Prop l s)) a
-> Map (Memo l s) (Prop l s) -> a
forall s a. State s a -> s -> a
`evalState` Map (Memo l s) (Prop l s)
forall k a. Map k a
M.empty) (State (Map (Memo l s) (Prop l s)) a -> a)
-> Diagram
     (Node l) Bool s Identity (State (Map (Memo l s) (Prop l s)) a)
-> Diagram (Node l) Bool s Identity a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram
     (Node l) Bool s Identity (State (Map (Memo l s) (Prop l s)) a)
forall (m :: * -> *) (f :: * -> *) a s b.
Monad m =>
Diagram f a s m b -> Diagram f a s Identity (m b)
D.compress (Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag Diagram l s a
forall s. Diagram l s a
d))

-- | A diagramatic proposition build on atomic propositions of type @l@
newtype Prop l s = Prop
  { Prop l s -> Free (Node l) Bool s
unProp :: D.Free (Node l) Bool s
  }
  deriving (Prop l s -> Prop l s -> Bool
(Prop l s -> Prop l s -> Bool)
-> (Prop l s -> Prop l s -> Bool) -> Eq (Prop l s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall l s. Prop l s -> Prop l s -> Bool
/= :: Prop l s -> Prop l s -> Bool
$c/= :: forall l s. Prop l s -> Prop l s -> Bool
== :: Prop l s -> Prop l s -> Bool
$c== :: forall l s. Prop l s -> Prop l s -> Bool
Eq, Eq (Prop l s)
Eq (Prop l s) =>
(Prop l s -> Prop l s -> Ordering)
-> (Prop l s -> Prop l s -> Bool)
-> (Prop l s -> Prop l s -> Bool)
-> (Prop l s -> Prop l s -> Bool)
-> (Prop l s -> Prop l s -> Bool)
-> (Prop l s -> Prop l s -> Prop l s)
-> (Prop l s -> Prop l s -> Prop l s)
-> Ord (Prop l s)
Prop l s -> Prop l s -> Bool
Prop l s -> Prop l s -> Ordering
Prop l s -> Prop l s -> Prop l s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall l s. Eq (Prop l s)
forall l s. Prop l s -> Prop l s -> Bool
forall l s. Prop l s -> Prop l s -> Ordering
forall l s. Prop l s -> Prop l s -> Prop l s
min :: Prop l s -> Prop l s -> Prop l s
$cmin :: forall l s. Prop l s -> Prop l s -> Prop l s
max :: Prop l s -> Prop l s -> Prop l s
$cmax :: forall l s. Prop l s -> Prop l s -> Prop l s
>= :: Prop l s -> Prop l s -> Bool
$c>= :: forall l s. Prop l s -> Prop l s -> Bool
> :: Prop l s -> Prop l s -> Bool
$c> :: forall l s. Prop l s -> Prop l s -> Bool
<= :: Prop l s -> Prop l s -> Bool
$c<= :: forall l s. Prop l s -> Prop l s -> Bool
< :: Prop l s -> Prop l s -> Bool
$c< :: forall l s. Prop l s -> Prop l s -> Bool
compare :: Prop l s -> Prop l s -> Ordering
$ccompare :: forall l s. Prop l s -> Prop l s -> Ordering
$cp1Ord :: forall l s. Eq (Prop l s)
Ord)

-- | An internal node of the diagram
data Node l k = Node
  { Node l k -> l
label :: l,
    Node l k -> k
lo :: k,
    Node l k -> k
hi :: k
  }
  deriving (a -> Node l b -> Node l a
(a -> b) -> Node l a -> Node l b
(forall a b. (a -> b) -> Node l a -> Node l b)
-> (forall a b. a -> Node l b -> Node l a) -> Functor (Node l)
forall a b. a -> Node l b -> Node l a
forall a b. (a -> b) -> Node l a -> Node l b
forall l a b. a -> Node l b -> Node l a
forall l a b. (a -> b) -> Node l a -> Node l b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Node l b -> Node l a
$c<$ :: forall l a b. a -> Node l b -> Node l a
fmap :: (a -> b) -> Node l a -> Node l b
$cfmap :: forall l a b. (a -> b) -> Node l a -> Node l b
Functor, Node l a -> Bool
(a -> m) -> Node l a -> m
(a -> b -> b) -> b -> Node l a -> b
(forall m. Monoid m => Node l m -> m)
-> (forall m a. Monoid m => (a -> m) -> Node l a -> m)
-> (forall m a. Monoid m => (a -> m) -> Node l a -> m)
-> (forall a b. (a -> b -> b) -> b -> Node l a -> b)
-> (forall a b. (a -> b -> b) -> b -> Node l a -> b)
-> (forall b a. (b -> a -> b) -> b -> Node l a -> b)
-> (forall b a. (b -> a -> b) -> b -> Node l a -> b)
-> (forall a. (a -> a -> a) -> Node l a -> a)
-> (forall a. (a -> a -> a) -> Node l a -> a)
-> (forall a. Node l a -> [a])
-> (forall a. Node l a -> Bool)
-> (forall a. Node l a -> Int)
-> (forall a. Eq a => a -> Node l a -> Bool)
-> (forall a. Ord a => Node l a -> a)
-> (forall a. Ord a => Node l a -> a)
-> (forall a. Num a => Node l a -> a)
-> (forall a. Num a => Node l a -> a)
-> Foldable (Node l)
forall a. Eq a => a -> Node l a -> Bool
forall a. Num a => Node l a -> a
forall a. Ord a => Node l a -> a
forall m. Monoid m => Node l m -> m
forall a. Node l a -> Bool
forall a. Node l a -> Int
forall a. Node l a -> [a]
forall a. (a -> a -> a) -> Node l a -> a
forall l a. Eq a => a -> Node l a -> Bool
forall l a. Num a => Node l a -> a
forall l a. Ord a => Node l a -> a
forall m a. Monoid m => (a -> m) -> Node l a -> m
forall l m. Monoid m => Node l m -> m
forall l a. Node l a -> Bool
forall l a. Node l a -> Int
forall l a. Node l a -> [a]
forall b a. (b -> a -> b) -> b -> Node l a -> b
forall a b. (a -> b -> b) -> b -> Node l a -> b
forall l a. (a -> a -> a) -> Node l a -> a
forall l m a. Monoid m => (a -> m) -> Node l a -> m
forall l b a. (b -> a -> b) -> b -> Node l a -> b
forall l a b. (a -> b -> b) -> b -> Node l a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Node l a -> a
$cproduct :: forall l a. Num a => Node l a -> a
sum :: Node l a -> a
$csum :: forall l a. Num a => Node l a -> a
minimum :: Node l a -> a
$cminimum :: forall l a. Ord a => Node l a -> a
maximum :: Node l a -> a
$cmaximum :: forall l a. Ord a => Node l a -> a
elem :: a -> Node l a -> Bool
$celem :: forall l a. Eq a => a -> Node l a -> Bool
length :: Node l a -> Int
$clength :: forall l a. Node l a -> Int
null :: Node l a -> Bool
$cnull :: forall l a. Node l a -> Bool
toList :: Node l a -> [a]
$ctoList :: forall l a. Node l a -> [a]
foldl1 :: (a -> a -> a) -> Node l a -> a
$cfoldl1 :: forall l a. (a -> a -> a) -> Node l a -> a
foldr1 :: (a -> a -> a) -> Node l a -> a
$cfoldr1 :: forall l a. (a -> a -> a) -> Node l a -> a
foldl' :: (b -> a -> b) -> b -> Node l a -> b
$cfoldl' :: forall l b a. (b -> a -> b) -> b -> Node l a -> b
foldl :: (b -> a -> b) -> b -> Node l a -> b
$cfoldl :: forall l b a. (b -> a -> b) -> b -> Node l a -> b
foldr' :: (a -> b -> b) -> b -> Node l a -> b
$cfoldr' :: forall l a b. (a -> b -> b) -> b -> Node l a -> b
foldr :: (a -> b -> b) -> b -> Node l a -> b
$cfoldr :: forall l a b. (a -> b -> b) -> b -> Node l a -> b
foldMap' :: (a -> m) -> Node l a -> m
$cfoldMap' :: forall l m a. Monoid m => (a -> m) -> Node l a -> m
foldMap :: (a -> m) -> Node l a -> m
$cfoldMap :: forall l m a. Monoid m => (a -> m) -> Node l a -> m
fold :: Node l m -> m
$cfold :: forall l m. Monoid m => Node l m -> m
Foldable, Functor (Node l)
Foldable (Node l)
(Functor (Node l), Foldable (Node l)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Node l a -> f (Node l b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Node l (f a) -> f (Node l a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Node l a -> m (Node l b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Node l (m a) -> m (Node l a))
-> Traversable (Node l)
(a -> f b) -> Node l a -> f (Node l b)
forall l. Functor (Node l)
forall l. Foldable (Node l)
forall l (m :: * -> *) a. Monad m => Node l (m a) -> m (Node l a)
forall l (f :: * -> *) a.
Applicative f =>
Node l (f a) -> f (Node l a)
forall l (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Node l a -> m (Node l b)
forall l (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Node l a -> f (Node l b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Node l (m a) -> m (Node l a)
forall (f :: * -> *) a.
Applicative f =>
Node l (f a) -> f (Node l a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Node l a -> m (Node l b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Node l a -> f (Node l b)
sequence :: Node l (m a) -> m (Node l a)
$csequence :: forall l (m :: * -> *) a. Monad m => Node l (m a) -> m (Node l a)
mapM :: (a -> m b) -> Node l a -> m (Node l b)
$cmapM :: forall l (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Node l a -> m (Node l b)
sequenceA :: Node l (f a) -> f (Node l a)
$csequenceA :: forall l (f :: * -> *) a.
Applicative f =>
Node l (f a) -> f (Node l a)
traverse :: (a -> f b) -> Node l a -> f (Node l b)
$ctraverse :: forall l (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Node l a -> f (Node l b)
$cp2Traversable :: forall l. Foldable (Node l)
$cp1Traversable :: forall l. Functor (Node l)
Traversable)

instance Eq l => Eq1 (Node l) where
  liftEq :: (a -> b -> Bool) -> Node l a -> Node l b -> Bool
liftEq eq :: a -> b -> Bool
eq n :: Node l a
n m :: Node l b
m = Node l a -> l
forall l k. Node l k -> l
label Node l a
n l -> l -> Bool
forall a. Eq a => a -> a -> Bool
== Node l b -> l
forall l k. Node l k -> l
label Node l b
m Bool -> Bool -> Bool
&& a -> b -> Bool
eq (Node l a -> a
forall l k. Node l k -> k
lo Node l a
n) (Node l b -> b
forall l k. Node l k -> k
lo Node l b
m) Bool -> Bool -> Bool
&& a -> b -> Bool
eq (Node l a -> a
forall l k. Node l k -> k
hi Node l a
n) (Node l b -> b
forall l k. Node l k -> k
hi Node l b
m)

instance Hashable l => Hashable1 (Node l) where
  liftHashWithSalt :: (Int -> a -> Int) -> Int -> Node l a -> Int
liftHashWithSalt l :: Int -> a -> Int
l s :: Int
s n :: Node l a
n = Int -> (l, Int, Int) -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Node l a -> l
forall l k. Node l k -> l
label Node l a
n, Int -> a -> Int
l Int
s (Node l a -> a
forall l k. Node l k -> k
lo Node l a
n), Int -> a -> Int
l Int
s (Node l a -> a
forall l k. Node l k -> k
hi Node l a
n))

-- | Make a proposition (if not already present) from it's lo and hi cases
mkProp :: (Eq l, Hashable l) => l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp :: l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp l :: l
l lo :: Prop l s
lo hi :: Prop l s
hi
  | Prop l s
lo Prop l s -> Prop l s -> Bool
forall a. Eq a => a -> a -> Bool
== Prop l s
hi = Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
lo
  | Bool
otherwise = Diagram
  (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Free (Node l) Bool s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Node l (Free (Node l) Bool s)
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Free (Node l) Bool s)
forall (m :: * -> *) (f :: * -> *) a s.
(Monad m, Hashable1 f, Hashable a, Eq1 f, Eq a) =>
f (Free f a s) -> Diagram f a s m (Free f a s)
D.free Node :: forall l k. l -> k -> k -> Node l k
Node {label :: l
label = l
l, lo :: Free (Node l) Bool s
lo = Prop l s -> Free (Node l) Bool s
forall l s. Prop l s -> Free (Node l) Bool s
unProp Prop l s
lo, hi :: Free (Node l) Bool s
hi = Prop l s -> Free (Node l) Bool s
forall l s. Prop l s -> Free (Node l) Bool s
unProp Prop l s
hi})

-- Map a function over a proposition but push the result through mkProp
mapProp :: (Eq l, Hashable l) => (Bool -> Bool) -> Prop l s -> Diagram l s (Prop l s)
mapProp :: (Bool -> Bool) -> Prop l s -> Diagram l s (Prop l s)
mapProp f :: Bool -> Bool
f (Prop p :: Free (Node l) Bool s
p) = Diagram
  (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
 -> Diagram l s (Prop l s))
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall a b. (a -> b) -> a -> b
$ (Node l (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Free (Node l) Bool s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) (f :: * -> *) b a s.
(Monad m, Traversable f) =>
(f b -> Diagram f a s m b)
-> (a -> Diagram f a s m b) -> Free f a s -> Diagram f a s m b
D.fold (\n :: Node l (Prop l s)
n -> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall a b. (a -> b) -> a -> b
$ l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp (Node l (Prop l s) -> l
forall l k. Node l k -> l
label Node l (Prop l s)
n) (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
lo Node l (Prop l s)
n) (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
hi Node l (Prop l s)
n)) (Prop l s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop l s
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool -> Prop l s)
-> Bool
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> (Bool -> Free (Node l) Bool s) -> Bool -> Prop l s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Free (Node l) Bool s
forall (f :: * -> *) a s. a -> Free f a s
D.Pure (Bool -> Free (Node l) Bool s)
-> (Bool -> Bool) -> Bool -> Free (Node l) Bool s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
f) Free (Node l) Bool s
p

-- | Map atoms in proposition
mapAtom :: (Eq l, Hashable l) => (l -> l) -> Prop l s -> Diagram l s (Prop l s)
mapAtom :: (l -> l) -> Prop l s -> Diagram l s (Prop l s)
mapAtom f :: l -> l
f (Prop p :: Free (Node l) Bool s
p) =
  Diagram
  (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
 -> Diagram l s (Prop l s))
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall a b. (a -> b) -> a -> b
$
    (Node l (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Free (Node l) Bool s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) (f :: * -> *) b a s.
(Monad m, Traversable f) =>
(f b -> Diagram f a s m b)
-> (a -> Diagram f a s m b) -> Free f a s -> Diagram f a s m b
D.fold
      ( \n :: Node l (Prop l s)
n -> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall a b. (a -> b) -> a -> b
$ do
          Prop l s
lo' <- (l -> l) -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
(l -> l) -> Prop l s -> Diagram l s (Prop l s)
mapAtom l -> l
f (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
lo Node l (Prop l s)
n)
          Prop l s
hi' <- (l -> l) -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
(l -> l) -> Prop l s -> Diagram l s (Prop l s)
mapAtom l -> l
f (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
hi Node l (Prop l s)
n)
          l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp (l -> l
f (l -> l) -> l -> l
forall a b. (a -> b) -> a -> b
$ Node l (Prop l s) -> l
forall l k. Node l k -> l
label Node l (Prop l s)
n) Prop l s
lo' Prop l s
hi'
      )
      (Prop l s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop l s
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool -> Prop l s)
-> Bool
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> (Bool -> Free (Node l) Bool s) -> Bool -> Prop l s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Free (Node l) Bool s
forall (f :: * -> *) a s. a -> Free f a s
D.Pure)
      Free (Node l) Bool s
p

-- | Replace an atom with a non-terminal in a 'Prop' sub-diagram
bindAtom :: (Ord l, Hashable l) => Prop l s -> (l -> Diagram l s (Prop l s)) -> Diagram l s (Prop l s)
bindAtom :: Prop l s -> (l -> Diagram l s (Prop l s)) -> Diagram l s (Prop l s)
bindAtom (Prop p :: Free (Node l) Bool s
p) f :: l -> Diagram l s (Prop l s)
f =
  Diagram
  (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
 -> Diagram l s (Prop l s))
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall a b. (a -> b) -> a -> b
$
    (Node l (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Free (Node l) Bool s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) (f :: * -> *) b a s.
(Monad m, Traversable f) =>
(f b -> Diagram f a s m b)
-> (a -> Diagram f a s m b) -> Free f a s -> Diagram f a s m b
D.fold
      ( \n :: Node l (Prop l s)
n -> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall a b. (a -> b) -> a -> b
$ do
          Prop l s
a <- l -> Diagram l s (Prop l s)
f (Node l (Prop l s) -> l
forall l k. Node l k -> l
label Node l (Prop l s)
n)
          Prop l s
b <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
(&&) Prop l s
a (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
hi Node l (Prop l s)
n)
          (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
(||) Prop l s
b (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
lo Node l (Prop l s)
n)
      )
      (Prop l s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop l s
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool -> Prop l s)
-> Bool
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> (Bool -> Free (Node l) Bool s) -> Bool -> Prop l s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Free (Node l) Bool s
forall (f :: * -> *) a s. a -> Free f a s
D.Pure)
      Free (Node l) Bool s
p

-- | Simple propositions
true, false :: Prop l s
true :: Prop l s
true = Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Bool -> Free (Node l) Bool s
forall (f :: * -> *) a s. a -> Free f a s
D.Pure Bool
True
false :: Prop l s
false = Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Bool -> Free (Node l) Bool s
forall (f :: * -> *) a s. a -> Free f a s
D.Pure Bool
False

-- | Construct a diagramatic proposition from an atom
atom, notAtom :: (Hashable l, Eq l) => l -> Diagram l s (Prop l s)
atom :: l -> Diagram l s (Prop l s)
atom l :: l
l = l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp l
l Prop l s
forall l s. Prop l s
false Prop l s
forall l s. Prop l s
true
notAtom :: l -> Diagram l s (Prop l s)
notAtom l :: l
l = l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp l
l Prop l s
forall l s. Prop l s
true Prop l s
forall l s. Prop l s
false

-- | Lift a binary operation on booleans to propositions
apply :: (Hashable l, Ord l) => (Bool -> Bool -> Bool) -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply :: (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply op :: Bool -> Bool -> Bool
op p :: Prop l s
p@(Prop p' :: Free (Node l) Bool s
p') q :: Prop l s
q@(Prop q' :: Free (Node l) Bool s
q') =
  Diagram
  (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
 -> Diagram l s (Prop l s))
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall a b. (a -> b) -> a -> b
$
    Free (Node l) Bool s
-> (Node l (Free (Node l) Bool s)
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) (f :: * -> *) a s b.
Monad m =>
Free f a s
-> (f (Free f a s) -> Diagram f a s m b)
-> (a -> Diagram f a s m b)
-> Diagram f a s m b
D.fromFree
      Free (Node l) Bool s
p'
      ( \n :: Node l (Free (Node l) Bool s)
n ->
          Free (Node l) Bool s
-> (Node l (Free (Node l) Bool s)
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) (f :: * -> *) a s b.
Monad m =>
Free f a s
-> (f (Free f a s) -> Diagram f a s m b)
-> (a -> Diagram f a s m b)
-> Diagram f a s m b
D.fromFree
            Free (Node l) Bool s
q'
            ( \m :: Node l (Free (Node l) Bool s)
m ->
                Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall a b. (a -> b) -> a -> b
$
                  case l -> l -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Node l (Free (Node l) Bool s) -> l
forall l k. Node l k -> l
label Node l (Free (Node l) Bool s)
n) (Node l (Free (Node l) Bool s) -> l
forall l k. Node l k -> l
label Node l (Free (Node l) Bool s)
m) of
                    LT -> do
                      Prop l s
lo' <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
op (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
lo Node l (Free (Node l) Bool s)
n) Prop l s
q
                      Prop l s
hi' <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
op (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
hi Node l (Free (Node l) Bool s)
n) Prop l s
q
                      l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp (Node l (Free (Node l) Bool s) -> l
forall l k. Node l k -> l
label Node l (Free (Node l) Bool s)
n) Prop l s
lo' Prop l s
hi'
                    EQ -> do
                      Prop l s
lo' <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
op (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
lo Node l (Free (Node l) Bool s)
n) (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
lo Node l (Free (Node l) Bool s)
m)
                      Prop l s
hi' <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
op (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
hi Node l (Free (Node l) Bool s)
n) (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
hi Node l (Free (Node l) Bool s)
m)
                      l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp (Node l (Free (Node l) Bool s) -> l
forall l k. Node l k -> l
label Node l (Free (Node l) Bool s)
n) Prop l s
lo' Prop l s
hi'
                    GT -> do
                      Prop l s
lo' <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
op Prop l s
p (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
lo Node l (Free (Node l) Bool s)
m)
                      Prop l s
hi' <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
op Prop l s
p (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> Free (Node l) Bool s -> Prop l s
forall a b. (a -> b) -> a -> b
$ Node l (Free (Node l) Bool s) -> Free (Node l) Bool s
forall l k. Node l k -> k
hi Node l (Free (Node l) Bool s)
m)
                      l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp (Node l (Free (Node l) Bool s) -> l
forall l k. Node l k -> l
label Node l (Free (Node l) Bool s)
m) Prop l s
lo' Prop l s
hi'
            )
            (\b :: Bool
b -> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
(Bool -> Bool) -> Prop l s -> Diagram l s (Prop l s)
mapProp (Bool -> Bool -> Bool
`op` Bool
b) Prop l s
p)
      )
      (\a :: Bool
a -> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
(Bool -> Bool) -> Prop l s -> Diagram l s (Prop l s)
mapProp (Bool -> Bool -> Bool
op Bool
a) Prop l s
q)

-- | Assign an atomic proposition a boolean value
restrict :: (Hashable l, Ord l) => l -> Bool -> Prop l s -> Diagram l s (Prop l s)
restrict :: l -> Bool -> Prop l s -> Diagram l s (Prop l s)
restrict l :: l
l b :: Bool
b (Prop p :: Free (Node l) Bool s
p) = do
  Map (Memo l s) (Prop l s)
memo <- Diagram
  (Node l)
  Bool
  s
  (State (Map (Memo l s) (Prop l s)))
  (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l)
   Bool
   s
   (State (Map (Memo l s) (Prop l s)))
   (Map (Memo l s) (Prop l s))
 -> Diagram l s (Map (Memo l s) (Prop l s)))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
forall s (m :: * -> *). MonadState s m => m s
get
  case Memo l s -> Map (Memo l s) (Prop l s) -> Maybe (Prop l s)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (l -> Bool -> Prop l s -> Memo l s
forall l s. l -> Bool -> Prop l s -> Memo l s
Restr l
l Bool
b (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop Free (Node l) Bool s
p)) Map (Memo l s) (Prop l s)
memo of
    Just r :: Prop l s
r -> Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r
    Nothing -> do
      Prop l s
r <-
        Diagram
  (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
 -> Diagram l s (Prop l s))
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
-> Diagram l s (Prop l s)
forall a b. (a -> b) -> a -> b
$
          (Node l (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool
    -> Diagram
         (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Free (Node l) Bool s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) (f :: * -> *) b a s.
(Monad m, Traversable f) =>
(f b -> Diagram f a s m b)
-> (a -> Diagram f a s m b) -> Free f a s -> Diagram f a s m b
D.fold
            ( \n :: Node l (Prop l s)
n ->
                if Node l (Prop l s) -> l
forall l k. Node l k -> l
label Node l (Prop l s)
n l -> l -> Bool
forall a. Eq a => a -> a -> Bool
== l
l
                  then if Bool
b then Prop l s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
hi Node l (Prop l s)
n) else Prop l s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
lo Node l (Prop l s)
n)
                  else Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s (Prop l s)
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> Diagram l s (Prop l s)
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall a b. (a -> b) -> a -> b
$ l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Eq l, Hashable l) =>
l -> Prop l s -> Prop l s -> Diagram l s (Prop l s)
mkProp (Node l (Prop l s) -> l
forall l k. Node l k -> l
label Node l (Prop l s)
n) (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
lo Node l (Prop l s)
n) (Node l (Prop l s) -> Prop l s
forall l k. Node l k -> k
hi Node l (Prop l s)
n)
            )
            (Prop l s
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop l s
 -> Diagram
      (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s))
-> (Bool -> Prop l s)
-> Bool
-> Diagram
     (Node l) Bool s (State (Map (Memo l s) (Prop l s))) (Prop l s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop (Free (Node l) Bool s -> Prop l s)
-> (Bool -> Free (Node l) Bool s) -> Bool -> Prop l s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Free (Node l) Bool s
forall (f :: * -> *) a s. a -> Free f a s
D.Pure)
            Free (Node l) Bool s
p
      Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
 -> Diagram l s ())
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State (Map (Memo l s) (Prop l s)) ()
 -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ())
-> State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall a b. (a -> b) -> a -> b
$ Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ())
-> Map (Memo l s) (Prop l s)
-> State (Map (Memo l s) (Prop l s)) ()
forall a b. (a -> b) -> a -> b
$ Memo l s
-> Prop l s
-> Map (Memo l s) (Prop l s)
-> Map (Memo l s) (Prop l s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (l -> Bool -> Prop l s -> Memo l s
forall l s. l -> Bool -> Prop l s -> Memo l s
Restr l
l Bool
b (Free (Node l) Bool s -> Prop l s
forall l s. Free (Node l) Bool s -> Prop l s
Prop Free (Node l) Bool s
p)) Prop l s
r Map (Memo l s) (Prop l s)
memo
      Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r

-- | Lift boolean and to diagramatic proposition
and :: (Ord l, Hashable l) => Prop l s -> Prop l s -> Diagram l s (Prop l s)
and :: Prop l s -> Prop l s -> Diagram l s (Prop l s)
and p :: Prop l s
p q :: Prop l s
q = do
  Map (Memo l s) (Prop l s)
memo <- Diagram
  (Node l)
  Bool
  s
  (State (Map (Memo l s) (Prop l s)))
  (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l)
   Bool
   s
   (State (Map (Memo l s) (Prop l s)))
   (Map (Memo l s) (Prop l s))
 -> Diagram l s (Map (Memo l s) (Prop l s)))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
forall s (m :: * -> *). MonadState s m => m s
get
  case Memo l s -> Map (Memo l s) (Prop l s) -> Maybe (Prop l s)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Prop l s -> Prop l s -> Memo l s
forall l s. Prop l s -> Prop l s -> Memo l s
And Prop l s
p Prop l s
q) Map (Memo l s) (Prop l s)
memo of
    Just r :: Prop l s
r -> Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r
    Nothing -> do
      Prop l s
r <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
(&&) Prop l s
p Prop l s
q
      Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
 -> Diagram l s ())
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State (Map (Memo l s) (Prop l s)) ()
 -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ())
-> State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall a b. (a -> b) -> a -> b
$ Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ())
-> Map (Memo l s) (Prop l s)
-> State (Map (Memo l s) (Prop l s)) ()
forall a b. (a -> b) -> a -> b
$ Memo l s
-> Prop l s
-> Map (Memo l s) (Prop l s)
-> Map (Memo l s) (Prop l s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Prop l s -> Prop l s -> Memo l s
forall l s. Prop l s -> Prop l s -> Memo l s
And Prop l s
p Prop l s
q) Prop l s
r Map (Memo l s) (Prop l s)
memo
      Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r

-- | Lift boolean or to diagramatic proposition
or :: (Ord l, Hashable l) => Prop l s -> Prop l s -> Diagram l s (Prop l s)
or :: Prop l s -> Prop l s -> Diagram l s (Prop l s)
or p :: Prop l s
p q :: Prop l s
q = do
  Map (Memo l s) (Prop l s)
memo <- Diagram
  (Node l)
  Bool
  s
  (State (Map (Memo l s) (Prop l s)))
  (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l)
   Bool
   s
   (State (Map (Memo l s) (Prop l s)))
   (Map (Memo l s) (Prop l s))
 -> Diagram l s (Map (Memo l s) (Prop l s)))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
forall s (m :: * -> *). MonadState s m => m s
get
  case Memo l s -> Map (Memo l s) (Prop l s) -> Maybe (Prop l s)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Prop l s -> Prop l s -> Memo l s
forall l s. Prop l s -> Prop l s -> Memo l s
Or Prop l s
p Prop l s
q) Map (Memo l s) (Prop l s)
memo of
    Just r :: Prop l s
r -> Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r
    Nothing -> do
      Prop l s
r <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply Bool -> Bool -> Bool
(||) Prop l s
p Prop l s
q
      Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
 -> Diagram l s ())
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State (Map (Memo l s) (Prop l s)) ()
 -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ())
-> State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall a b. (a -> b) -> a -> b
$ Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ())
-> Map (Memo l s) (Prop l s)
-> State (Map (Memo l s) (Prop l s)) ()
forall a b. (a -> b) -> a -> b
$ Memo l s
-> Prop l s
-> Map (Memo l s) (Prop l s)
-> Map (Memo l s) (Prop l s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Prop l s -> Prop l s -> Memo l s
forall l s. Prop l s -> Prop l s -> Memo l s
Or Prop l s
p Prop l s
q) Prop l s
r Map (Memo l s) (Prop l s)
memo
      Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r

-- | Lift boolean not to diagramatic proposition
not :: (Ord l, Hashable l) => Prop l s -> Diagram l s (Prop l s)
not :: Prop l s -> Diagram l s (Prop l s)
not p :: Prop l s
p = do
  Map (Memo l s) (Prop l s)
memo <- Diagram
  (Node l)
  Bool
  s
  (State (Map (Memo l s) (Prop l s)))
  (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram
   (Node l)
   Bool
   s
   (State (Map (Memo l s) (Prop l s)))
   (Map (Memo l s) (Prop l s))
 -> Diagram l s (Map (Memo l s) (Prop l s)))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
-> Diagram l s (Map (Memo l s) (Prop l s))
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
-> Diagram
     (Node l)
     Bool
     s
     (State (Map (Memo l s) (Prop l s)))
     (Map (Memo l s) (Prop l s))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift State (Map (Memo l s) (Prop l s)) (Map (Memo l s) (Prop l s))
forall s (m :: * -> *). MonadState s m => m s
get
  case Memo l s -> Map (Memo l s) (Prop l s) -> Maybe (Prop l s)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Prop l s -> Memo l s
forall l s. Prop l s -> Memo l s
Not Prop l s
p) Map (Memo l s) (Prop l s)
memo of
    Just r :: Prop l s
r -> Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r
    Nothing -> do
      Prop l s
r <- (Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
forall l s.
(Hashable l, Ord l) =>
(Bool -> Bool -> Bool)
-> Prop l s -> Prop l s -> Diagram l s (Prop l s)
apply (\a :: Bool
a b :: Bool
b -> Bool -> Bool
Prelude.not Bool
a Bool -> Bool -> Bool
&& Bool -> Bool
Prelude.not Bool
b) Prop l s
p Prop l s
p
      Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
 -> Diagram l s ())
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
-> Diagram l s ()
forall a b. (a -> b) -> a -> b
$ State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (State (Map (Memo l s) (Prop l s)) ()
 -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ())
-> State (Map (Memo l s) (Prop l s)) ()
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) ()
forall a b. (a -> b) -> a -> b
$ Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Map (Memo l s) (Prop l s) -> State (Map (Memo l s) (Prop l s)) ())
-> Map (Memo l s) (Prop l s)
-> State (Map (Memo l s) (Prop l s)) ()
forall a b. (a -> b) -> a -> b
$ Memo l s
-> Prop l s
-> Map (Memo l s) (Prop l s)
-> Map (Memo l s) (Prop l s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Prop l s -> Memo l s
forall l s. Prop l s -> Memo l s
Not Prop l s
p) Prop l s
r Map (Memo l s) (Prop l s)
memo
      Prop l s -> Diagram l s (Prop l s)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop l s
r

-- | Determine if a proposition is satisfiable
--
--     >  anySat = fold (\_ p q -> p || q) id
anySat :: (Hashable l, Eq l) => Prop l s -> Diagram l s Bool
anySat :: Prop l s -> Diagram l s Bool
anySat = (l -> Bool -> Bool -> Diagram l s Bool)
-> (Bool -> Diagram l s Bool) -> Prop l s -> Diagram l s Bool
forall l b s.
(Hashable l, Eq l) =>
(l -> b -> b -> Diagram l s b)
-> (Bool -> Diagram l s b) -> Prop l s -> Diagram l s b
fold (\_ p :: Bool
p q :: Bool
q -> Bool -> Diagram l s Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
p Bool -> Bool -> Bool
|| Bool
q)) Bool -> Diagram l s Bool
forall (m :: * -> *) a. Monad m => a -> m a
return

-- | Create a summary value of a proposition
fold :: (Hashable l, Eq l) => (l -> b -> b -> Diagram l s b) -> (Bool -> Diagram l s b) -> Prop l s -> Diagram l s b
fold :: (l -> b -> b -> Diagram l s b)
-> (Bool -> Diagram l s b) -> Prop l s -> Diagram l s b
fold f :: l -> b -> b -> Diagram l s b
f g :: Bool -> Diagram l s b
g (Prop p :: Free (Node l) Bool s
p) = Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
-> Diagram l s b
forall l s a.
Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
-> Diagram l s a
Diagram (Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
 -> Diagram l s b)
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
-> Diagram l s b
forall a b. (a -> b) -> a -> b
$ (Node l b
 -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b)
-> (Bool
    -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b)
-> Free (Node l) Bool s
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
forall (m :: * -> *) (f :: * -> *) b a s.
(Monad m, Traversable f) =>
(f b -> Diagram f a s m b)
-> (a -> Diagram f a s m b) -> Free f a s -> Diagram f a s m b
D.fold (\n :: Node l b
n -> Diagram l s b
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s b
 -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b)
-> Diagram l s b
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
forall a b. (a -> b) -> a -> b
$ l -> b -> b -> Diagram l s b
f (Node l b -> l
forall l k. Node l k -> l
label Node l b
n) (Node l b -> b
forall l k. Node l k -> k
lo Node l b
n) (Node l b -> b
forall l k. Node l k -> k
hi Node l b
n)) (Diagram l s b
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
forall l s a.
Diagram l s a
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) a
unDiag (Diagram l s b
 -> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b)
-> (Bool -> Diagram l s b)
-> Bool
-> Diagram (Node l) Bool s (State (Map (Memo l s) (Prop l s))) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Diagram l s b
g) Free (Node l) Bool s
p