module SMCDEL.Internal.TaggedBDD where

import Data.Tagged
import Data.HasCacBDD hiding (Top,Bot)

import SMCDEL.Language

-- * Tagged BDDs

-- | Operations on tagged BDDs.
-- The tag `a` is meant to be an empty type.
class TagForBDDs a where
  -- | How many copies of the vocabulary do we have?
  -- This is the number of markers + 1.
  multiplier :: Tagged a Bdd -> Int
  multiplier Tagged a Bdd
_ = Int
2
  -- | Move back, must be without markers!
  unmvBdd :: Tagged a Bdd -> Bdd
  unmvBdd = (Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> if Int -> Bool
forall a. Integral a => a -> Bool
even Int
n then Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2 else [Char] -> Int
forall a. HasCallStack => [Char] -> a
error ([Char]
"Odd: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)) (Bdd -> Bdd) -> (Tagged a Bdd -> Bdd) -> Tagged a Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged a Bdd -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag
  -- | Move into double vocabulary, but do not add marker
  mv :: Bdd -> Tagged a Bdd
  mv = Int -> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Int -> Bdd -> Tagged a Bdd
cpMany Int
0
  -- | Move into extended vocabulary, add one marker
  cp :: Bdd -> Tagged a Bdd
  cp = Int -> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Int -> Bdd -> Tagged a Bdd
cpMany Int
1
  -- | Move into extended vocabulary, add k many markers, MUST be available!
  cpMany :: Int -> Bdd -> Tagged a Bdd
  cpMany Int
k Bdd
b = let x :: Tagged a Bdd
x = Bdd -> Tagged a Bdd
forall a. a -> Tagged a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bdd -> Tagged a Bdd) -> Bdd -> Tagged a Bdd
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k) Bdd
b
                in if Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Tagged a Bdd -> Int
forall a. TagForBDDs a => Tagged a Bdd -> Int
multiplier Tagged a Bdd
x then [Char] -> Tagged a Bdd
forall a. HasCallStack => [Char] -> a
error [Char]
"Not enough markers!" else Tagged a Bdd
x

  -- | Evaluate a tagged BDD.
  tagBddEval :: [Prp] -> Tagged a Bdd -> Bool
  tagBddEval [Prp]
truths Tagged a Bdd
querybdd = Bdd -> (Int -> Bool) -> Bool
evaluateFun (Tagged a Bdd -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag Tagged a Bdd
querybdd) (\Int
n -> Int -> Prp
P Int
n Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
truths)

-- * Pre-defined tags

-- | Tag for BDDs using the duplicated vocabulary \(V \cup V'\).
data Dubbel
instance TagForBDDs Dubbel where
  multiplier :: Tagged Dubbel Bdd -> Int
multiplier = Int -> Tagged Dubbel Bdd -> Int
forall a b. a -> b -> a
const Int
2

-- | Tag for BDDs using the triple vocabulary \(V \cup V' \cup V''\).
data Tripel
instance TagForBDDs Tripel where
  multiplier :: Tagged Tripel Bdd -> Int
multiplier = Int -> Tagged Tripel Bdd -> Int
forall a b. a -> b -> a
const Int
3

-- | Tag for BDDs using the quadruple vocabulary \(V \cup V' \cup V'' \cup V'''\).
data Quadrupel
instance TagForBDDs Quadrupel where
  multiplier :: Tagged Quadrupel Bdd -> Int
multiplier = Int -> Tagged Quadrupel Bdd -> Int
forall a b. a -> b -> a
const Int
4

-- * Generic definition for tagged BDDs

-- | The total relation as a tagged BDD.
totalRelBdd :: Tagged a Bdd
totalRelBdd :: forall a. Tagged a Bdd
totalRelBdd = Bdd -> Tagged a Bdd
forall a. a -> Tagged a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
top

-- | The empty relation as a tagged BDD.
emptyRelBdd :: Tagged a Bdd
emptyRelBdd :: forall a. Tagged a Bdd
emptyRelBdd = Bdd -> Tagged a Bdd
forall a. a -> Tagged a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
bot

-- | Given a vocabulary, make a tagged BDD to say
-- that each plain variable \(p\) and the corresponding
-- marked variable \(p'\) variable have the same value:
-- \( \wedge_p (p \leftrightarrow p') \).
-- This encodes the identity relation.
allsamebdd :: TagForBDDs a => [Prp] -> Tagged a Bdd
allsamebdd :: forall a. TagForBDDs a => [Prp] -> Tagged a Bdd
allsamebdd [Prp]
ps = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> Tagged a [Bdd] -> Tagged a Bdd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Tagged a Bdd] -> Tagged a [Bdd]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ Bdd -> Bdd -> Bdd
equ (Bdd -> Bdd -> Bdd) -> Tagged a Bdd -> Tagged a (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
mv (Int -> Bdd
var Int
x) Tagged a (Bdd -> Bdd) -> Tagged a Bdd -> Tagged a Bdd
forall a b. Tagged a (a -> b) -> Tagged a a -> Tagged a b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
cp (Int -> Bdd
var Int
x) | (P Int
x) <- [Prp]
ps ]