{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StrictData #-}

-- | Boolean expressions implemented using naive trees
module Data.Algebra.Boolean
  ( Parser,
    CTX,
    Expr,
    eval,
    expr,
  )
where

import Control.Applicative.Combinators.NonEmpty (sepBy1)
import Data.Char
import Data.Foldable
import Data.List.NonEmpty
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Text (Text, unpack)
import Data.Void
import Text.Megaparsec hiding (sepBy1)
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L

type Parser = Parsec Void Text

newtype Var = Var Text
  deriving newtype (Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq Var
Ord)

-- | Context. Every variable not in context will be treated as False.
type CTX = Map Text Bool

data Expr
  = BNeg Expr
  | BVar Var
  | BConj Expr Expr
  | BDisj Expr Expr
  deriving (Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq)

instance Show Expr where
  showsPrec :: Int -> Expr -> ShowS
showsPrec Int
_ (BVar (Var Text
v)) = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$ Text -> String
unpack Text
v
  showsPrec Int
p (BNeg Expr
expr') =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"¬" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Expr -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 Expr
expr'
  showsPrec Int
p (BConj Expr
expr1 Expr
expr2) =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      Int -> Expr -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 Expr
expr1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ∧ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Expr -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 Expr
expr2
  showsPrec Int
p (BDisj Expr
expr1 Expr
expr2) =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      Int -> Expr -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
1 Expr
expr1 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" ∨ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Expr -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
1 Expr
expr2

-- | Evaluate an expression in a context.
eval :: CTX -> Expr -> Bool
eval :: CTX -> Expr -> Bool
eval CTX
ctx Expr
e
  | BNeg Expr
e' <- Expr
e = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CTX -> Expr -> Bool
eval CTX
ctx Expr
e'
  | BVar Var
v <- Expr
e = Var -> Bool
lkup Var
v
  | BConj Expr
e1 Expr
e2 <- Expr
e = CTX -> Expr -> Bool
eval CTX
ctx Expr
e1 Bool -> Bool -> Bool
&& CTX -> Expr -> Bool
eval CTX
ctx Expr
e2
  | BDisj Expr
e1 Expr
e2 <- Expr
e = CTX -> Expr -> Bool
eval CTX
ctx Expr
e1 Bool -> Bool -> Bool
|| CTX -> Expr -> Bool
eval CTX
ctx Expr
e2
  where
    lkup :: Var -> Bool
    lkup :: Var -> Bool
lkup (Var Text
v) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Text -> CTX -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
v CTX
ctx

symbol :: Text -> Parser Text
symbol :: Text -> Parser Text
symbol = ParsecT Void Text Identity ()
-> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
m () -> Tokens s -> m (Tokens s)
L.symbol ParsecT Void Text Identity ()
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space

lexeme :: Parser a -> Parser a
lexeme :: Parser a -> Parser a
lexeme = ParsecT Void Text Identity () -> Parser a -> Parser a
forall e s (m :: Type -> Type) a.
MonadParsec e s m =>
m () -> m a -> m a
L.lexeme ParsecT Void Text Identity ()
forall e s (m :: Type -> Type).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space

paren :: Parser a -> Parser a
paren :: Parser a -> Parser a
paren = Parser Text -> Parser Text -> Parser a -> Parser a
forall (m :: Type -> Type) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (Text -> Parser Text
symbol Text
"(") (Text -> Parser Text
symbol Text
")")

conj :: Parser Char
conj :: Parser Char
conj = Parser Char -> Parser Char
forall a. Parser a -> Parser a
lexeme (Parser Char -> Parser Char) -> Parser Char -> Parser Char
forall a b. (a -> b) -> a -> b
$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Token s -> m (Token s)
single Char
Token Text
'&' Parser Char -> Parser Char -> Parser Char
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Token s -> m (Token s)
single Char
Token Text
'∧'

disj :: Parser Char
disj :: Parser Char
disj = Parser Char -> Parser Char
forall a. Parser a -> Parser a
lexeme (Parser Char -> Parser Char) -> Parser Char -> Parser Char
forall a b. (a -> b) -> a -> b
$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Token s -> m (Token s)
single Char
Token Text
'|' Parser Char -> Parser Char -> Parser Char
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Token s -> m (Token s)
single Char
Token Text
'∨'

neg :: Parser Char
neg :: Parser Char
neg = Parser Char -> Parser Char
forall a. Parser a -> Parser a
lexeme (Parser Char -> Parser Char) -> Parser Char -> Parser Char
forall a b. (a -> b) -> a -> b
$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Token s -> m (Token s)
single Char
Token Text
'!' Parser Char -> Parser Char -> Parser Char
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Token s -> m (Token s)
single Char
Token Text
'¬'

conjList :: NonEmpty Expr -> Expr
conjList :: NonEmpty Expr -> Expr
conjList (Expr
h :| [Expr]
l) = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> Expr -> Expr
BConj Expr
h [Expr]
l

disjList :: NonEmpty Expr -> Expr
disjList :: NonEmpty Expr -> Expr
disjList (Expr
h :| [Expr]
l) = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> Expr -> Expr
BDisj Expr
h [Expr]
l

neg' :: Parser Expr
neg' :: Parser Expr
neg' = Parser Expr -> Parser Expr
forall e s (m :: Type -> Type) a. MonadParsec e s m => m a -> m a
try Parser Expr
negated Parser Expr -> Parser Expr -> Parser Expr
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
normal
  where
    negated :: Parser Expr
negated = do
      Char
_ <- Parser Char
neg
      Expr -> Expr
BNeg (Expr -> Expr) -> Parser Expr -> Parser Expr
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
term
    normal :: Parser Expr
normal = Parser Expr
term

conj' :: Parser Expr
conj' :: Parser Expr
conj' = NonEmpty Expr -> Expr
conjList (NonEmpty Expr -> Expr)
-> ParsecT Void Text Identity (NonEmpty Expr) -> Parser Expr
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
-> Parser Char -> ParsecT Void Text Identity (NonEmpty Expr)
forall (m :: Type -> Type) a sep.
Alternative m =>
m a -> m sep -> m (NonEmpty a)
sepBy1 Parser Expr
neg' Parser Char
conj

var :: Parser Expr
var :: Parser Expr
var = Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
lexeme (Parser Expr -> Parser Expr) -> Parser Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Var -> Expr
BVar (Var -> Expr) -> (Text -> Var) -> Text -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Var
Var (Text -> Expr) -> Parser Text -> Parser Expr
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
-> (Token Text -> Bool) -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: Type -> Type).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhile1P (String -> Maybe String
forall a. a -> Maybe a
Just String
"variable") Char -> Bool
Token Text -> Bool
isAlphaNum

term :: Parser Expr
term :: Parser Expr
term = Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
paren Parser Expr
expr Parser Expr -> Parser Expr -> Parser Expr
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
var

-- | Parse an expression
expr :: Parser Expr
expr :: Parser Expr
expr = NonEmpty Expr -> Expr
disjList (NonEmpty Expr -> Expr)
-> ParsecT Void Text Identity (NonEmpty Expr) -> Parser Expr
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
-> Parser Char -> ParsecT Void Text Identity (NonEmpty Expr)
forall (m :: Type -> Type) a sep.
Alternative m =>
m a -> m sep -> m (NonEmpty a)
sepBy1 Parser Expr
conj' Parser Char
disj