{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : Data.ZSDD.Internal
-- Copyright   : (c) Eddie Jones 2020
-- License     : BSD-3
-- Maintainer  : eddiejones2108@gmail.com
-- Stability   : experimental
--
-- = WARNING
--
-- This module is __internal__ and may be frequently changed.
module Data.ZSDD.Internal
  ( -- * Diagrams
    Diagram (..),
    Ops (..),
    runDiagram,

    -- * Internal Nodes
    ID,
    Node (..),
    withNode,
    insertNode,
    lookupNode,

    -- * Propositions
    Prop (..),
    Invertible (..),
    makeProp,

    -- ** Construction
    -- $construction
    atomic,
    negate,
    assign,
    union,
    intersect,
    difference,

    -- ** Query
    isEmpty,
    isNotEmpty,
    count,

    -- ** Map
    mapAtom,
    bindAtom,
  )
where

import Control.Monad
import Control.Monad.State
import qualified Data.HashMap.Lazy as H
import Data.Hashable
import qualified Data.IntMap as I
import GHC.Generics (Generic)
import Prelude hiding (map, negate)

-- | A unique node identifier
type ID = Int

-- | A proposition parameterised by it's diagram and atom type
data Prop d a
  = Top
  | Bot
  | ID ID
  deriving (Prop d a -> Prop d a -> Bool
(Prop d a -> Prop d a -> Bool)
-> (Prop d a -> Prop d a -> Bool) -> Eq (Prop d a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall d a. Prop d a -> Prop d a -> Bool
/= :: Prop d a -> Prop d a -> Bool
$c/= :: forall d a. Prop d a -> Prop d a -> Bool
== :: Prop d a -> Prop d a -> Bool
$c== :: forall d a. Prop d a -> Prop d a -> Bool
Eq, Eq (Prop d a)
Eq (Prop d a) =>
(Prop d a -> Prop d a -> Ordering)
-> (Prop d a -> Prop d a -> Bool)
-> (Prop d a -> Prop d a -> Bool)
-> (Prop d a -> Prop d a -> Bool)
-> (Prop d a -> Prop d a -> Bool)
-> (Prop d a -> Prop d a -> Prop d a)
-> (Prop d a -> Prop d a -> Prop d a)
-> Ord (Prop d a)
Prop d a -> Prop d a -> Bool
Prop d a -> Prop d a -> Ordering
Prop d a -> Prop d a -> Prop d a
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 d a. Eq (Prop d a)
forall d a. Prop d a -> Prop d a -> Bool
forall d a. Prop d a -> Prop d a -> Ordering
forall d a. Prop d a -> Prop d a -> Prop d a
min :: Prop d a -> Prop d a -> Prop d a
$cmin :: forall d a. Prop d a -> Prop d a -> Prop d a
max :: Prop d a -> Prop d a -> Prop d a
$cmax :: forall d a. Prop d a -> Prop d a -> Prop d a
>= :: Prop d a -> Prop d a -> Bool
$c>= :: forall d a. Prop d a -> Prop d a -> Bool
> :: Prop d a -> Prop d a -> Bool
$c> :: forall d a. Prop d a -> Prop d a -> Bool
<= :: Prop d a -> Prop d a -> Bool
$c<= :: forall d a. Prop d a -> Prop d a -> Bool
< :: Prop d a -> Prop d a -> Bool
$c< :: forall d a. Prop d a -> Prop d a -> Bool
compare :: Prop d a -> Prop d a -> Ordering
$ccompare :: forall d a. Prop d a -> Prop d a -> Ordering
$cp1Ord :: forall d a. Eq (Prop d a)
Ord, (forall x. Prop d a -> Rep (Prop d a) x)
-> (forall x. Rep (Prop d a) x -> Prop d a) -> Generic (Prop d a)
forall x. Rep (Prop d a) x -> Prop d a
forall x. Prop d a -> Rep (Prop d a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall d a x. Rep (Prop d a) x -> Prop d a
forall d a x. Prop d a -> Rep (Prop d a) x
$cto :: forall d a x. Rep (Prop d a) x -> Prop d a
$cfrom :: forall d a x. Prop d a -> Rep (Prop d a) x
Generic)

instance Hashable (Prop d a)

-- | An internal node of the diagram graph
data Node d a = Node
  { Node d a -> a
atom :: a,
    Node d a -> Prop d a
lo :: Prop d a,
    Node d a -> Prop d a
hi :: Prop d a
  }
  deriving (Node d a -> Node d a -> Bool
(Node d a -> Node d a -> Bool)
-> (Node d a -> Node d a -> Bool) -> Eq (Node d a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall d a. Eq a => Node d a -> Node d a -> Bool
/= :: Node d a -> Node d a -> Bool
$c/= :: forall d a. Eq a => Node d a -> Node d a -> Bool
== :: Node d a -> Node d a -> Bool
$c== :: forall d a. Eq a => Node d a -> Node d a -> Bool
Eq, (forall x. Node d a -> Rep (Node d a) x)
-> (forall x. Rep (Node d a) x -> Node d a) -> Generic (Node d a)
forall x. Rep (Node d a) x -> Node d a
forall x. Node d a -> Rep (Node d a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall d a x. Rep (Node d a) x -> Node d a
forall d a x. Node d a -> Rep (Node d a) x
$cto :: forall d a x. Rep (Node d a) x -> Node d a
$cfrom :: forall d a x. Node d a -> Rep (Node d a) x
Generic)

instance Hashable a => Hashable (Node d a)

-- | Atom types where every atom has an inverse.
-- This is only required by the difference operation
class Invertible a where
  neg :: a -> a

-- | The ambient decision diagram of propositions.
--
-- The type parameter d is the diagrams existential labelled and should not be instantiated by a concrete type
newtype Diagram d a m r = Diagram
  { Diagram d a m r
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     r
getState ::
      StateT
        ( ID, -- Fresh node ID
          H.HashMap (Ops a) (Prop d a), -- Cached operations
          H.HashMap (Node d a) Int, -- node to ID
          I.IntMap (Node d a) -- ID to node
        )
        m
        r
  }
  deriving (a -> Diagram d a m b -> Diagram d a m a
(a -> b) -> Diagram d a m a -> Diagram d a m b
(forall a b. (a -> b) -> Diagram d a m a -> Diagram d a m b)
-> (forall a b. a -> Diagram d a m b -> Diagram d a m a)
-> Functor (Diagram d a m)
forall a b. a -> Diagram d a m b -> Diagram d a m a
forall a b. (a -> b) -> Diagram d a m a -> Diagram d a m b
forall d a (m :: * -> *) a b.
Functor m =>
a -> Diagram d a m b -> Diagram d a m a
forall d a (m :: * -> *) a b.
Functor m =>
(a -> b) -> Diagram d a m a -> Diagram d a m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Diagram d a m b -> Diagram d a m a
$c<$ :: forall d a (m :: * -> *) a b.
Functor m =>
a -> Diagram d a m b -> Diagram d a m a
fmap :: (a -> b) -> Diagram d a m a -> Diagram d a m b
$cfmap :: forall d a (m :: * -> *) a b.
Functor m =>
(a -> b) -> Diagram d a m a -> Diagram d a m b
Functor, Functor (Diagram d a m)
a -> Diagram d a m a
Functor (Diagram d a m) =>
(forall a. a -> Diagram d a m a)
-> (forall a b.
    Diagram d a m (a -> b) -> Diagram d a m a -> Diagram d a m b)
-> (forall a b c.
    (a -> b -> c)
    -> Diagram d a m a -> Diagram d a m b -> Diagram d a m c)
-> (forall a b.
    Diagram d a m a -> Diagram d a m b -> Diagram d a m b)
-> (forall a b.
    Diagram d a m a -> Diagram d a m b -> Diagram d a m a)
-> Applicative (Diagram d a m)
Diagram d a m a -> Diagram d a m b -> Diagram d a m b
Diagram d a m a -> Diagram d a m b -> Diagram d a m a
Diagram d a m (a -> b) -> Diagram d a m a -> Diagram d a m b
(a -> b -> c)
-> Diagram d a m a -> Diagram d a m b -> Diagram d a m c
forall a. a -> Diagram d a m a
forall a b. Diagram d a m a -> Diagram d a m b -> Diagram d a m a
forall a b. Diagram d a m a -> Diagram d a m b -> Diagram d a m b
forall a b.
Diagram d a m (a -> b) -> Diagram d a m a -> Diagram d a m b
forall a b c.
(a -> b -> c)
-> Diagram d a m a -> Diagram d a m b -> Diagram d a m c
forall d a (m :: * -> *). Monad m => Functor (Diagram d a m)
forall d a (m :: * -> *) a. Monad m => a -> Diagram d a m a
forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> Diagram d a m b -> Diagram d a m a
forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> Diagram d a m b -> Diagram d a m b
forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m (a -> b) -> Diagram d a m a -> Diagram d a m b
forall d a (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> Diagram d a m a -> Diagram d a m b -> Diagram d a m 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 d a m a -> Diagram d a m b -> Diagram d a m a
$c<* :: forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> Diagram d a m b -> Diagram d a m a
*> :: Diagram d a m a -> Diagram d a m b -> Diagram d a m b
$c*> :: forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> Diagram d a m b -> Diagram d a m b
liftA2 :: (a -> b -> c)
-> Diagram d a m a -> Diagram d a m b -> Diagram d a m c
$cliftA2 :: forall d a (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> Diagram d a m a -> Diagram d a m b -> Diagram d a m c
<*> :: Diagram d a m (a -> b) -> Diagram d a m a -> Diagram d a m b
$c<*> :: forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m (a -> b) -> Diagram d a m a -> Diagram d a m b
pure :: a -> Diagram d a m a
$cpure :: forall d a (m :: * -> *) a. Monad m => a -> Diagram d a m a
$cp1Applicative :: forall d a (m :: * -> *). Monad m => Functor (Diagram d a m)
Applicative, Applicative (Diagram d a m)
a -> Diagram d a m a
Applicative (Diagram d a m) =>
(forall a b.
 Diagram d a m a -> (a -> Diagram d a m b) -> Diagram d a m b)
-> (forall a b.
    Diagram d a m a -> Diagram d a m b -> Diagram d a m b)
-> (forall a. a -> Diagram d a m a)
-> Monad (Diagram d a m)
Diagram d a m a -> (a -> Diagram d a m b) -> Diagram d a m b
Diagram d a m a -> Diagram d a m b -> Diagram d a m b
forall a. a -> Diagram d a m a
forall a b. Diagram d a m a -> Diagram d a m b -> Diagram d a m b
forall a b.
Diagram d a m a -> (a -> Diagram d a m b) -> Diagram d a m b
forall d a (m :: * -> *). Monad m => Applicative (Diagram d a m)
forall d a (m :: * -> *) a. Monad m => a -> Diagram d a m a
forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> Diagram d a m b -> Diagram d a m b
forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> (a -> Diagram d a m b) -> Diagram d a m 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 d a m a
$creturn :: forall d a (m :: * -> *) a. Monad m => a -> Diagram d a m a
>> :: Diagram d a m a -> Diagram d a m b -> Diagram d a m b
$c>> :: forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> Diagram d a m b -> Diagram d a m b
>>= :: Diagram d a m a -> (a -> Diagram d a m b) -> Diagram d a m b
$c>>= :: forall d a (m :: * -> *) a b.
Monad m =>
Diagram d a m a -> (a -> Diagram d a m b) -> Diagram d a m b
$cp1Monad :: forall d a (m :: * -> *). Monad m => Applicative (Diagram d a m)
Monad)

-- | Operation DSL for cache
data Ops a
  = Atomic a
  | Union ID ID
  | Intersect ID ID
  | Difference ID ID
  | DifferenceT ID
  | Negate ID a
  | Assign ID a Bool
  deriving (Ops a -> Ops a -> Bool
(Ops a -> Ops a -> Bool) -> (Ops a -> Ops a -> Bool) -> Eq (Ops a)
forall a. Eq a => Ops a -> Ops a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ops a -> Ops a -> Bool
$c/= :: forall a. Eq a => Ops a -> Ops a -> Bool
== :: Ops a -> Ops a -> Bool
$c== :: forall a. Eq a => Ops a -> Ops a -> Bool
Eq, Eq (Ops a)
Eq (Ops a) =>
(Ops a -> Ops a -> Ordering)
-> (Ops a -> Ops a -> Bool)
-> (Ops a -> Ops a -> Bool)
-> (Ops a -> Ops a -> Bool)
-> (Ops a -> Ops a -> Bool)
-> (Ops a -> Ops a -> Ops a)
-> (Ops a -> Ops a -> Ops a)
-> Ord (Ops a)
Ops a -> Ops a -> Bool
Ops a -> Ops a -> Ordering
Ops a -> Ops a -> Ops a
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 a. Ord a => Eq (Ops a)
forall a. Ord a => Ops a -> Ops a -> Bool
forall a. Ord a => Ops a -> Ops a -> Ordering
forall a. Ord a => Ops a -> Ops a -> Ops a
min :: Ops a -> Ops a -> Ops a
$cmin :: forall a. Ord a => Ops a -> Ops a -> Ops a
max :: Ops a -> Ops a -> Ops a
$cmax :: forall a. Ord a => Ops a -> Ops a -> Ops a
>= :: Ops a -> Ops a -> Bool
$c>= :: forall a. Ord a => Ops a -> Ops a -> Bool
> :: Ops a -> Ops a -> Bool
$c> :: forall a. Ord a => Ops a -> Ops a -> Bool
<= :: Ops a -> Ops a -> Bool
$c<= :: forall a. Ord a => Ops a -> Ops a -> Bool
< :: Ops a -> Ops a -> Bool
$c< :: forall a. Ord a => Ops a -> Ops a -> Bool
compare :: Ops a -> Ops a -> Ordering
$ccompare :: forall a. Ord a => Ops a -> Ops a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Ops a)
Ord, (forall x. Ops a -> Rep (Ops a) x)
-> (forall x. Rep (Ops a) x -> Ops a) -> Generic (Ops a)
forall x. Rep (Ops a) x -> Ops a
forall x. Ops a -> Rep (Ops a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Ops a) x -> Ops a
forall a x. Ops a -> Rep (Ops a) x
$cto :: forall a x. Rep (Ops a) x -> Ops a
$cfrom :: forall a x. Ops a -> Rep (Ops a) x
Generic)

instance Hashable a => Hashable (Ops a)

-- | Extract information that does not depend on the digram
runDiagram :: Monad m => (forall d. Diagram d a m r) -> m r
runDiagram :: (forall d. Diagram d a m r) -> m r
runDiagram (Diagram f) = StateT
  (Int, HashMap (Ops a) (Prop Any a), HashMap (Node Any a) Int,
   IntMap (Node Any a))
  m
  r
-> (Int, HashMap (Ops a) (Prop Any a), HashMap (Node Any a) Int,
    IntMap (Node Any a))
-> m r
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT
  (Int, HashMap (Ops a) (Prop Any a), HashMap (Node Any a) Int,
   IntMap (Node Any a))
  m
  r
f (0, HashMap (Ops a) (Prop Any a)
forall k v. HashMap k v
H.empty, HashMap (Node Any a) Int
forall k v. HashMap k v
H.empty, IntMap (Node Any a)
forall a. IntMap a
I.empty)

-- Lookup operation in cache and run otherwise
memo :: (Ord a, Hashable a, Monad m) => Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo :: Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo o :: Ops a
o k :: Diagram d a m (Prop d a)
k = StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Prop d a)
-> Diagram d a m (Prop d a)
forall d a (m :: * -> *) r.
StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  r
-> Diagram d a m r
Diagram (StateT
   (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
    IntMap (Node d a))
   m
   (Prop d a)
 -> Diagram d a m (Prop d a))
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     (Prop d a)
-> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$ do
  (_, mem :: HashMap (Ops a) (Prop d a)
mem, _, _) <- StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
forall s (m :: * -> *). MonadState s m => m s
get
  case Ops a -> HashMap (Ops a) (Prop d a) -> Maybe (Prop d a)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
H.lookup Ops a
o HashMap (Ops a) (Prop d a)
mem of
    Nothing -> do
      Prop d a
p <- Diagram d a m (Prop d a)
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     (Prop d a)
forall d a (m :: * -> *) r.
Diagram d a m r
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     r
getState Diagram d a m (Prop d a)
k
      (i :: Int
i, mem' :: HashMap (Ops a) (Prop d a)
mem', h :: HashMap (Node d a) Int
h, ns :: IntMap (Node d a)
ns) <- StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
forall s (m :: * -> *). MonadState s m => m s
get
      (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
 IntMap (Node d a))
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
i, Ops a
-> Prop d a
-> HashMap (Ops a) (Prop d a)
-> HashMap (Ops a) (Prop d a)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
H.insert Ops a
o Prop d a
p HashMap (Ops a) (Prop d a)
mem', HashMap (Node d a) Int
h, IntMap (Node d a)
ns)
      Prop d a
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
    Just p :: Prop d a
p -> Prop d a
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p

-- Get a fresh id
fresh :: Monad m => Diagram d a m ID
fresh :: Diagram d a m Int
fresh = StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  Int
-> Diagram d a m Int
forall d a (m :: * -> *) r.
StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  r
-> Diagram d a m r
Diagram (StateT
   (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
    IntMap (Node d a))
   m
   Int
 -> Diagram d a m Int)
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     Int
-> Diagram d a m Int
forall a b. (a -> b) -> a -> b
$ do
  (i :: Int
i, mem :: HashMap (Ops a) (Prop d a)
mem, h :: HashMap (Node d a) Int
h, ns :: IntMap (Node d a)
ns) <- StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
forall s (m :: * -> *). MonadState s m => m s
get
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
 IntMap (Node d a))
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1, HashMap (Ops a) (Prop d a)
mem, HashMap (Node d a) Int
h, IntMap (Node d a)
ns)
  Int
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

-- | Extract internal node information from it's ID
withNode :: Monad m => ID -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode :: Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode i :: Int
i f :: Node d a -> Diagram d a m r
f = StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  r
-> Diagram d a m r
forall d a (m :: * -> *) r.
StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  r
-> Diagram d a m r
Diagram (StateT
   (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
    IntMap (Node d a))
   m
   r
 -> Diagram d a m r)
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     r
-> Diagram d a m r
forall a b. (a -> b) -> a -> b
$ do
  (_, _, _, ns :: IntMap (Node d a)
ns) <- StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
forall s (m :: * -> *). MonadState s m => m s
get
  case Int -> IntMap (Node d a) -> Maybe (Node d a)
forall a. Int -> IntMap a -> Maybe a
I.lookup Int
i IntMap (Node d a)
ns of
    Nothing -> [Char]
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     r
forall a. HasCallStack => [Char] -> a
error ("Node not found!")
    Just n :: Node d a
n -> Diagram d a m r
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     r
forall d a (m :: * -> *) r.
Diagram d a m r
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     r
getState (Diagram d a m r
 -> StateT
      (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
       IntMap (Node d a))
      m
      r)
-> Diagram d a m r
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     r
forall a b. (a -> b) -> a -> b
$ Node d a -> Diagram d a m r
f Node d a
n

-- | Insert a new node
insertNode :: (Eq a, Hashable a, Monad m) => ID -> Node d a -> Diagram d a m ()
insertNode :: Int -> Node d a -> Diagram d a m ()
insertNode i :: Int
i n :: Node d a
n = StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  ()
-> Diagram d a m ()
forall d a (m :: * -> *) r.
StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  r
-> Diagram d a m r
Diagram (StateT
   (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
    IntMap (Node d a))
   m
   ()
 -> Diagram d a m ())
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     ()
-> Diagram d a m ()
forall a b. (a -> b) -> a -> b
$ do
  (j :: Int
j, m :: HashMap (Ops a) (Prop d a)
m, h :: HashMap (Node d a) Int
h, ns :: IntMap (Node d a)
ns) <- StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
forall s (m :: * -> *). MonadState s m => m s
get
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
 IntMap (Node d a))
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
j, HashMap (Ops a) (Prop d a)
m, Node d a -> Int -> HashMap (Node d a) Int -> HashMap (Node d a) Int
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
H.insert Node d a
n Int
i HashMap (Node d a) Int
h, Int -> Node d a -> IntMap (Node d a) -> IntMap (Node d a)
forall a. Int -> a -> IntMap a -> IntMap a
I.insert Int
i Node d a
n IntMap (Node d a)
ns)

-- | Find the ID of an existing node
lookupNode :: (Eq a, Hashable a, Monad m) => Node d a -> Diagram d a m (Maybe ID)
lookupNode :: Node d a -> Diagram d a m (Maybe Int)
lookupNode n :: Node d a
n = StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Maybe Int)
-> Diagram d a m (Maybe Int)
forall d a (m :: * -> *) r.
StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  r
-> Diagram d a m r
Diagram (StateT
   (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
    IntMap (Node d a))
   m
   (Maybe Int)
 -> Diagram d a m (Maybe Int))
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     (Maybe Int)
-> Diagram d a m (Maybe Int)
forall a b. (a -> b) -> a -> b
$ do
  (_, _, h :: HashMap (Node d a) Int
h, _) <- StateT
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
  m
  (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
   IntMap (Node d a))
forall s (m :: * -> *). MonadState s m => m s
get
  Maybe Int
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int
 -> StateT
      (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
       IntMap (Node d a))
      m
      (Maybe Int))
-> Maybe Int
-> StateT
     (Int, HashMap (Ops a) (Prop d a), HashMap (Node d a) Int,
      IntMap (Node d a))
     m
     (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Node d a -> HashMap (Node d a) Int -> Maybe Int
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
H.lookup Node d a
n HashMap (Node d a) Int
h

-- | Make a new proposition (if not already present) from a node
makeProp :: (Eq a, Hashable a, Monad m) => Node d a -> Diagram d a m (Prop d a)
makeProp :: Node d a -> Diagram d a m (Prop d a)
makeProp n :: Node d a
n
  | Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n Prop d a -> Prop d a -> Bool
forall a. Eq a => a -> a -> Bool
== Prop d a
forall d a. Prop d a
Bot = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n) -- Node elimination
  | Bool
otherwise = Node d a -> Diagram d a m (Maybe Int)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Maybe Int)
lookupNode Node d a
n Diagram d a m (Maybe Int)
-> (Maybe Int -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just i :: Int
i -> Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Prop d a
forall d a. Int -> Prop d a
ID Int
i)
    Nothing -> do
      Int
i <- Diagram d a m Int
forall (m :: * -> *) d a. Monad m => Diagram d a m Int
fresh
      Int -> Node d a -> Diagram d a m ()
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Int -> Node d a -> Diagram d a m ()
insertNode Int
i Node d a
n
      Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Prop d a
forall d a. Int -> Prop d a
ID Int
i)

-- $construction
-- Non-trivial propositions are constructed within a diagram.
-- Although propositions use information from the diagram, they are independant;
-- each operation is applied to the supplied proposition leaving others untouched.

-- | Construct a proposition from an atom
atomic :: (Ord a, Hashable a, Monad m) => a -> Diagram d a m (Prop d a)
atomic :: a -> Diagram d a m (Prop d a)
atomic a :: a
a =
  Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo (a -> Ops a
forall a. a -> Ops a
Atomic a
a) (Diagram d a m (Prop d a) -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$
    Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node {atom :: a
atom = a
a, lo :: Prop d a
lo = Prop d a
forall d a. Prop d a
Bot, hi :: Prop d a
hi = Prop d a
forall d a. Prop d a
Top}

-- | Instantiating an atom
assign :: (Ord a, Hashable a, Monad m) => Prop d a -> a -> Bool -> Diagram d a m (Prop d a)
assign :: Prop d a -> a -> Bool -> Diagram d a m (Prop d a)
assign Top _ _ = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Top
assign Bot _ _ = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
assign (ID i :: Int
i) var :: a
var b :: Bool
b =
  Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo (Int -> a -> Bool -> Ops a
forall a. Int -> a -> Bool -> Ops a
Assign Int
i a
var Bool
b) (Diagram d a m (Prop d a) -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$
    Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode
      Int
i
      ( \n :: Node d a
n ->
          case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Node d a -> a
forall d a. Node d a -> a
atom Node d a
n) a
var of
            LT -> Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
            EQ -> Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n)
            GT -> do
              Prop d a
lo' <- Prop d a -> a -> Bool -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> a -> Bool -> Diagram d a m (Prop d a)
assign (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n) a
var Bool
b
              Prop d a
hi' <- Prop d a -> a -> Bool -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> a -> Bool -> Diagram d a m (Prop d a)
assign (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n) a
var Bool
b
              Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                  { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
                    lo :: Prop d a
lo = Prop d a
lo',
                    hi :: Prop d a
hi = Prop d a
hi'
                  }
      )

-- | Negate every occurance of an atom
negate :: (Ord a, Hashable a, Monad m) => Prop d a -> a -> Diagram d a m (Prop d a)
negate :: Prop d a -> a -> Diagram d a m (Prop d a)
negate Top _ = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Top
negate Bot _ = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
negate p :: Prop d a
p@(ID i :: Int
i) var :: a
var =
  Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo (Int -> a -> Ops a
forall a. Int -> a -> Ops a
Negate Int
i a
var) (Diagram d a m (Prop d a) -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$
    Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode
      Int
i
      ( \n :: Node d a
n ->
          case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Node d a -> a
forall d a. Node d a -> a
atom Node d a
n) a
var of
            LT ->
              Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                  { atom :: a
atom = a
var,
                    lo :: Prop d a
lo = Prop d a
forall d a. Prop d a
Bot,
                    hi :: Prop d a
hi = Prop d a
p
                  }
            EQ ->
              Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                  { atom :: a
atom = a
var,
                    lo :: Prop d a
lo = Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n,
                    hi :: Prop d a
hi = Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n
                  }
            GT -> do
              Prop d a
lo' <- Prop d a -> a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> a -> Diagram d a m (Prop d a)
negate (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n) a
var
              Prop d a
hi' <- Prop d a -> a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> a -> Diagram d a m (Prop d a)
negate (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n) a
var
              Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                  { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
                    lo :: Prop d a
lo = Prop d a
lo',
                    hi :: Prop d a
hi = Prop d a
hi'
                  }
      )

-- | Union of two propositions
union :: (Ord a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a)
union :: Prop d a -> Prop d a -> Diagram d a m (Prop d a)
union Top _ = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Top
union _ Top = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Top
union Bot q :: Prop d a
q = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
q
union p :: Prop d a
p Bot = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
union p :: Prop d a
p q :: Prop d a
q | Prop d a
p Prop d a -> Prop d a -> Bool
forall a. Eq a => a -> a -> Bool
== Prop d a
q = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
union p :: Prop d a
p@(ID i :: Int
i) (ID j :: Int
j) =
  Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo (Int -> Int -> Ops a
forall a. Int -> Int -> Ops a
Union Int
i Int
j) (Diagram d a m (Prop d a) -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$
    Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode
      Int
i
      ( \n :: Node d a
n ->
          Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
j ((Node d a -> Diagram d a m (Prop d a))
 -> Diagram d a m (Prop d a))
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$ \m :: Node d a
m ->
            case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Node d a -> a
forall d a. Node d a -> a
atom Node d a
n) (Node d a -> a
forall d a. Node d a -> a
atom Node d a
m) of
              LT -> do
                Prop d a
lo' <- Prop d a
p Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`union` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
m
                Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                  Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                    { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
m,
                      lo :: Prop d a
lo = Prop d a
lo',
                      hi :: Prop d a
hi = Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
m
                    }
              EQ -> do
                Prop d a
lo' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`union` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
m
                Prop d a
hi' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`union` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
m
                Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                  Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                    { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
                      lo :: Prop d a
lo = Prop d a
lo',
                      hi :: Prop d a
hi = Prop d a
hi'
                    }
              GT -> do
                Prop d a
lo' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`union` Prop d a
p
                Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                  Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                    { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
                      lo :: Prop d a
lo = Prop d a
lo',
                      hi :: Prop d a
hi = Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n
                    }
      )

-- | Intersection of two propositions
intersect :: (Ord a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a)
intersect :: Prop d a -> Prop d a -> Diagram d a m (Prop d a)
intersect Top p :: Prop d a
p = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
intersect p :: Prop d a
p Top = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
intersect Bot _ = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
intersect _ Bot = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
intersect p :: Prop d a
p q :: Prop d a
q | Prop d a
p Prop d a -> Prop d a -> Bool
forall a. Eq a => a -> a -> Bool
== Prop d a
q = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
intersect p :: Prop d a
p@(ID i :: Int
i) q :: Prop d a
q@(ID j :: Int
j) =
  Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo (Int -> Int -> Ops a
forall a. Int -> Int -> Ops a
Intersect Int
i Int
j) (Diagram d a m (Prop d a) -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$
    Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode
      Int
i
      ( \n :: Node d a
n ->
          Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
j ((Node d a -> Diagram d a m (Prop d a))
 -> Diagram d a m (Prop d a))
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$ \m :: Node d a
m ->
            case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Node d a -> a
forall d a. Node d a -> a
atom Node d a
n) (Node d a -> a
forall d a. Node d a -> a
atom Node d a
m) of
              LT -> Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`intersect` Prop d a
q
              EQ -> do
                Prop d a
lo' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`intersect` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
m
                Prop d a
hi' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`intersect` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
m
                Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                  Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                    { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
                      lo :: Prop d a
lo = Prop d a
lo',
                      hi :: Prop d a
hi = Prop d a
hi'
                    }
              GT -> Prop d a
p Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`intersect` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
m
      )

-- | Difference between two propositions
difference :: (Ord a, Invertible a, Hashable a, Monad m) => Prop d a -> Prop d a -> Diagram d a m (Prop d a)
difference :: Prop d a -> Prop d a -> Diagram d a m (Prop d a)
difference _ Top = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
difference Bot _ = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
difference p :: Prop d a
p Bot = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
difference p :: Prop d a
p q :: Prop d a
q | Prop d a
p Prop d a -> Prop d a -> Bool
forall a. Eq a => a -> a -> Bool
== Prop d a
q = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
p
difference Top (ID j :: Int
j) =
  Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo (Int -> Ops a
forall a. Int -> Ops a
DifferenceT Int
j) (Diagram d a m (Prop d a) -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$
    Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode
      Int
j
      ( \m :: Node d a
m ->
          Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
            Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
              { atom :: a
atom = a -> a
forall a. Invertible a => a -> a
neg (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Node d a -> a
forall d a. Node d a -> a
atom Node d a
m,
                lo :: Prop d a
lo = Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
m,
                hi :: Prop d a
hi = Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
m
              }
      )
difference p :: Prop d a
p@(ID i :: Int
i) q :: Prop d a
q@(ID j :: Int
j) =
  Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Hashable a, Monad m) =>
Ops a -> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
memo (Int -> Int -> Ops a
forall a. Int -> Int -> Ops a
Difference Int
i Int
j) (Diagram d a m (Prop d a) -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a) -> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$
    Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode
      Int
i
      ( \n :: Node d a
n ->
          Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
j ((Node d a -> Diagram d a m (Prop d a))
 -> Diagram d a m (Prop d a))
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$ \m :: Node d a
m ->
            case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Node d a -> a
forall d a. Node d a -> a
atom Node d a
n) (Node d a -> a
forall d a. Node d a -> a
atom Node d a
m) of
              LT -> Prop d a
p Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Invertible a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`difference` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
m
              EQ -> do
                Prop d a
lo' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Invertible a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`difference` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
m
                Prop d a
hi' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Invertible a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`difference` Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
m
                Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                  Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                    { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
                      lo :: Prop d a
lo = Prop d a
lo',
                      hi :: Prop d a
hi = Prop d a
hi'
                    }
              GT -> do
                Prop d a
lo' <- Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Ord a, Invertible a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Diagram d a m (Prop d a)
`difference` Prop d a
q
                Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
                  Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
                    { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
                      lo :: Prop d a
lo = Prop d a
lo',
                      hi :: Prop d a
hi = Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n
                    }
      )

-- | Does the proposition have any models?
isEmpty, isNotEmpty :: Monad m => Prop d a -> Diagram d a m Bool
isEmpty :: Prop d a -> Diagram d a m Bool
isEmpty Bot = Bool -> Diagram d a m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isEmpty Top = Bool -> Diagram d a m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isEmpty (ID i :: Int
i) = Int -> (Node d a -> Diagram d a m Bool) -> Diagram d a m Bool
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
i ((Node d a -> Diagram d a m Bool) -> Diagram d a m Bool)
-> (Node d a -> Diagram d a m Bool) -> Diagram d a m Bool
forall a b. (a -> b) -> a -> b
$ \n :: Node d a
n -> do
  Bool
p <- Prop d a -> Diagram d a m Bool
forall (m :: * -> *) d a. Monad m => Prop d a -> Diagram d a m Bool
isEmpty (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n)
  Bool
q <- Prop d a -> Diagram d a m Bool
forall (m :: * -> *) d a. Monad m => Prop d a -> Diagram d a m Bool
isEmpty (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n)
  Bool -> Diagram d a m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
p Bool -> Bool -> Bool
&& Bool
q)
isNotEmpty :: Prop d a -> Diagram d a m Bool
isNotEmpty Bot = Bool -> Diagram d a m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isNotEmpty Top = Bool -> Diagram d a m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isNotEmpty (ID i :: Int
i) = Int -> (Node d a -> Diagram d a m Bool) -> Diagram d a m Bool
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
i ((Node d a -> Diagram d a m Bool) -> Diagram d a m Bool)
-> (Node d a -> Diagram d a m Bool) -> Diagram d a m Bool
forall a b. (a -> b) -> a -> b
$ \n :: Node d a
n -> do
  Bool
p <- Prop d a -> Diagram d a m Bool
forall (m :: * -> *) d a. Monad m => Prop d a -> Diagram d a m Bool
isNotEmpty (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n)
  Bool
q <- Prop d a -> Diagram d a m Bool
forall (m :: * -> *) d a. Monad m => Prop d a -> Diagram d a m Bool
isNotEmpty (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n)
  Bool -> Diagram d a m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
p Bool -> Bool -> Bool
|| Bool
q)

-- | Count the number of models
count :: Monad m => Prop d a -> Diagram d a m Int
count :: Prop d a -> Diagram d a m Int
count Bot = Int -> Diagram d a m Int
forall (m :: * -> *) a. Monad m => a -> m a
return 0
count Top = Int -> Diagram d a m Int
forall (m :: * -> *) a. Monad m => a -> m a
return 1
count (ID i :: Int
i) = Int -> (Node d a -> Diagram d a m Int) -> Diagram d a m Int
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
i ((Node d a -> Diagram d a m Int) -> Diagram d a m Int)
-> (Node d a -> Diagram d a m Int) -> Diagram d a m Int
forall a b. (a -> b) -> a -> b
$ \n :: Node d a
n -> do
  Int
x <- Prop d a -> Diagram d a m Int
forall (m :: * -> *) d a. Monad m => Prop d a -> Diagram d a m Int
count (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n)
  Int
y <- Prop d a -> Diagram d a m Int
forall (m :: * -> *) d a. Monad m => Prop d a -> Diagram d a m Int
count (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n)
  Int -> Diagram d a m Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y)

-- | Map between atoms
mapAtom :: (Eq a, Hashable a, Monad m) => (a -> a) -> Prop d a -> Diagram d a m (Prop d a)
mapAtom :: (a -> a) -> Prop d a -> Diagram d a m (Prop d a)
mapAtom _ Top = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Top
mapAtom _ Bot = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
mapAtom f :: a -> a
f (ID i :: Int
i) = Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
i ((Node d a -> Diagram d a m (Prop d a))
 -> Diagram d a m (Prop d a))
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$ \n :: Node d a
n -> do
  Prop d a
lo' <- (a -> a) -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
(a -> a) -> Prop d a -> Diagram d a m (Prop d a)
mapAtom a -> a
f (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n)
  Prop d a
hi' <- (a -> a) -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
(a -> a) -> Prop d a -> Diagram d a m (Prop d a)
mapAtom a -> a
f (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n)
  Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
    Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
      { atom :: a
atom = a -> a
f (Node d a -> a
forall d a. Node d a -> a
atom Node d a
n),
        lo :: Prop d a
lo = Prop d a
lo',
        hi :: Prop d a
hi = Prop d a
hi'
      }

-- Loop continuations to another part of the diagram
mapTerminal :: (Eq a, Hashable a, Monad m) => Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
mapTerminal :: Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
mapTerminal top :: Prop d a
top _ Top = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
top
mapTerminal _ bot :: Prop d a
bot Bot = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
bot
mapTerminal top :: Prop d a
top bot :: Prop d a
bot (ID i :: Int
i) = Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
i ((Node d a -> Diagram d a m (Prop d a))
 -> Diagram d a m (Prop d a))
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$ \n :: Node d a
n -> do
  Prop d a
lo' <- Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
mapTerminal Prop d a
top Prop d a
bot (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n)
  Prop d a
hi' <- Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
mapTerminal Prop d a
top Prop d a
bot (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n)
  Node d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Node d a -> Diagram d a m (Prop d a)
makeProp
    Node :: forall d a. a -> Prop d a -> Prop d a -> Node d a
Node
      { atom :: a
atom = Node d a -> a
forall d a. Node d a -> a
atom Node d a
n,
        lo :: Prop d a
lo = Prop d a
lo',
        hi :: Prop d a
hi = Prop d a
hi'
      }

-- | Instantiate an atom with a non-atomic proposition
bindAtom :: (Eq a, Hashable a, Monad m) => (a -> Diagram d a m (Prop d a)) -> Prop d a -> Diagram d a m (Prop d a)
bindAtom :: (a -> Diagram d a m (Prop d a))
-> Prop d a -> Diagram d a m (Prop d a)
bindAtom _ Top = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Top
bindAtom _ Bot = Prop d a -> Diagram d a m (Prop d a)
forall (m :: * -> *) a. Monad m => a -> m a
return Prop d a
forall d a. Prop d a
Bot
bindAtom f :: a -> Diagram d a m (Prop d a)
f (ID i :: Int
i) = Int
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall (m :: * -> *) d a r.
Monad m =>
Int -> (Node d a -> Diagram d a m r) -> Diagram d a m r
withNode Int
i ((Node d a -> Diagram d a m (Prop d a))
 -> Diagram d a m (Prop d a))
-> (Node d a -> Diagram d a m (Prop d a))
-> Diagram d a m (Prop d a)
forall a b. (a -> b) -> a -> b
$ \n :: Node d a
n -> do
  Prop d a
lo' <- (a -> Diagram d a m (Prop d a))
-> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
(a -> Diagram d a m (Prop d a))
-> Prop d a -> Diagram d a m (Prop d a)
bindAtom a -> Diagram d a m (Prop d a)
f (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
lo Node d a
n)
  Prop d a
hi' <- (a -> Diagram d a m (Prop d a))
-> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
(a -> Diagram d a m (Prop d a))
-> Prop d a -> Diagram d a m (Prop d a)
bindAtom a -> Diagram d a m (Prop d a)
f (Node d a -> Prop d a
forall d a. Node d a -> Prop d a
hi Node d a
n)
  Prop d a
p <- a -> Diagram d a m (Prop d a)
f (Node d a -> a
forall d a. Node d a -> a
atom Node d a
n)
  Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
forall a (m :: * -> *) d.
(Eq a, Hashable a, Monad m) =>
Prop d a -> Prop d a -> Prop d a -> Diagram d a m (Prop d a)
mapTerminal Prop d a
lo' Prop d a
hi' Prop d a
p