{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Formula
-- Copyright   :  (c) Masahiro Sakai 2012-2021
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Formula
  (
  -- * Boolean formula type
    Formula (Atom, And, Or, Not, Equiv, Imply, ITE)
  , fold
  , evalFormula
  , simplify
  ) where

import Control.Monad
import Control.Monad.ST
import qualified Data.Aeson as J
import Data.Aeson ((.=))
import Data.Hashable
import qualified Data.HashTable.Class as H
import qualified Data.HashTable.ST.Cuckoo as C
import Data.Interned
import GHC.Generics
import ToySolver.Data.Boolean
import qualified ToySolver.Data.BoolExpr as BoolExpr
import qualified ToySolver.SAT.Types as SAT
import ToySolver.SAT.Internal.JSON

-- Should this module be merged into ToySolver.SAT.Types module?

-- ------------------------------------------------------------------------

-- | Arbitrary formula not restricted to CNF
data Formula = Formula {-# UNPACK #-} !Id UFormula

instance Eq Formula where
  Formula Lit
i UFormula
_ == :: Formula -> Formula -> Bool
== Formula Lit
j UFormula
_ = Lit
i Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
j

instance Show Formula where
  showsPrec :: Lit -> Formula -> ShowS
showsPrec Lit
d Formula
x = Lit -> BoolExpr Lit -> ShowS
forall a. Show a => Lit -> a -> ShowS
showsPrec Lit
d (Formula -> BoolExpr Lit
toBoolExpr Formula
x)

instance Read Formula where
  readsPrec :: Lit -> ReadS Formula
readsPrec Lit
d String
s = [(BoolExpr Lit -> Formula
fromBoolExpr BoolExpr Lit
b, String
rest) | (BoolExpr Lit
b, String
rest) <- Lit -> ReadS (BoolExpr Lit)
forall a. Read a => Lit -> ReadS a
readsPrec Lit
d String
s]

instance Hashable Formula where
  hashWithSalt :: Lit -> Formula -> Lit
hashWithSalt Lit
s (Formula Lit
i UFormula
_) = Lit -> Lit -> Lit
forall a. Hashable a => Lit -> a -> Lit
hashWithSalt Lit
s Lit
i

data UFormula
  = UAtom SAT.Lit
  | UAnd [Formula]
  | UOr [Formula]
  | UNot Formula
  | UImply Formula Formula
  | UEquiv Formula Formula
  | UITE Formula Formula Formula

instance Interned Formula where
  type Uninterned Formula = UFormula
  data Description Formula
    = DAtom SAT.Lit
    | DAnd [Id]
    | DOr [Id]
    | DNot Id
    | DImply Id Id
    | DEquiv Id Id
    | DITE Id Id Id
    deriving (Description Formula -> Description Formula -> Bool
(Description Formula -> Description Formula -> Bool)
-> (Description Formula -> Description Formula -> Bool)
-> Eq (Description Formula)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Description Formula -> Description Formula -> Bool
== :: Description Formula -> Description Formula -> Bool
$c/= :: Description Formula -> Description Formula -> Bool
/= :: Description Formula -> Description Formula -> Bool
Eq, (forall x. Description Formula -> Rep (Description Formula) x)
-> (forall x. Rep (Description Formula) x -> Description Formula)
-> Generic (Description Formula)
forall x. Rep (Description Formula) x -> Description Formula
forall x. Description Formula -> Rep (Description Formula) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Description Formula -> Rep (Description Formula) x
from :: forall x. Description Formula -> Rep (Description Formula) x
$cto :: forall x. Rep (Description Formula) x -> Description Formula
to :: forall x. Rep (Description Formula) x -> Description Formula
Generic)
  describe :: Uninterned Formula -> Description Formula
describe (UAtom Lit
a) = Lit -> Description Formula
DAtom Lit
a
  describe (UAnd [Formula]
xs) = [Lit] -> Description Formula
DAnd [Lit
i | Formula Lit
i UFormula
_ <- [Formula]
xs]
  describe (UOr [Formula]
xs) = [Lit] -> Description Formula
DOr [Lit
i | Formula Lit
i UFormula
_ <- [Formula]
xs]
  describe (UNot (Formula Lit
i UFormula
_)) = Lit -> Description Formula
DNot Lit
i
  describe (UImply (Formula Lit
i UFormula
_) (Formula Lit
j UFormula
_)) = Lit -> Lit -> Description Formula
DImply Lit
i Lit
j
  describe (UEquiv (Formula Lit
i UFormula
_) (Formula Lit
j UFormula
_)) = Lit -> Lit -> Description Formula
DEquiv Lit
i Lit
j
  describe (UITE (Formula Lit
i UFormula
_) (Formula Lit
j UFormula
_) (Formula Lit
k UFormula
_)) = Lit -> Lit -> Lit -> Description Formula
DITE Lit
i Lit
j Lit
k
  identify :: Lit -> Uninterned Formula -> Formula
identify = Lit -> Uninterned Formula -> Formula
Lit -> UFormula -> Formula
Formula
  cache :: Cache Formula
cache = Cache Formula
formulaCache

instance Hashable (Description Formula)

instance Uninternable Formula where
  unintern :: Formula -> Uninterned Formula
unintern (Formula Lit
_ UFormula
uformula) = Uninterned Formula
UFormula
uformula

formulaCache :: Cache Formula
formulaCache :: Cache Formula
formulaCache = Cache Formula
forall t. Interned t => Cache t
mkCache
{-# NOINLINE formulaCache #-}

-- ------------------------------------------------------------------------

pattern Atom :: SAT.Lit -> Formula
pattern $mAtom :: forall {r}. Formula -> (Lit -> r) -> ((# #) -> r) -> r
$bAtom :: Lit -> Formula
Atom l <- (unintern -> UAtom l) where
  Atom Lit
l = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Lit -> UFormula
UAtom Lit
l)

pattern Not :: Formula -> Formula
pattern $mNot :: forall {r}. Formula -> (Formula -> r) -> ((# #) -> r) -> r
$bNot :: Formula -> Formula
Not p <- (unintern -> UNot p) where
  Not Formula
p = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> UFormula
UNot Formula
p)

pattern And :: [Formula] -> Formula
pattern $mAnd :: forall {r}. Formula -> ([Formula] -> r) -> ((# #) -> r) -> r
$bAnd :: [Formula] -> Formula
And ps <- (unintern -> UAnd ps) where
  And [Formula]
ps = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern ([Formula] -> UFormula
UAnd [Formula]
ps)

pattern Or :: [Formula] -> Formula
pattern $mOr :: forall {r}. Formula -> ([Formula] -> r) -> ((# #) -> r) -> r
$bOr :: [Formula] -> Formula
Or ps <- (unintern -> UOr ps) where
  Or [Formula]
ps = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern ([Formula] -> UFormula
UOr [Formula]
ps)

pattern Equiv :: Formula -> Formula -> Formula
pattern $mEquiv :: forall {r}.
Formula -> (Formula -> Formula -> r) -> ((# #) -> r) -> r
$bEquiv :: Formula -> Formula -> Formula
Equiv p q <- (unintern -> UEquiv p q) where
  Equiv Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UEquiv Formula
p Formula
q)

pattern Imply :: Formula -> Formula -> Formula
pattern $mImply :: forall {r}.
Formula -> (Formula -> Formula -> r) -> ((# #) -> r) -> r
$bImply :: Formula -> Formula -> Formula
Imply p q <- (unintern -> UImply p q) where
  Imply Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UImply Formula
p Formula
q)

pattern ITE :: Formula -> Formula -> Formula -> Formula
pattern $mITE :: forall {r}.
Formula
-> (Formula -> Formula -> Formula -> r) -> ((# #) -> r) -> r
$bITE :: Formula -> Formula -> Formula -> Formula
ITE p q r <- (unintern -> UITE p q r) where
  ITE Formula
p Formula
q Formula
r = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> Formula -> UFormula
UITE Formula
p Formula
q Formula
r)

{-# COMPLETE Atom, Not, And, Or, Equiv, Imply, ITE #-}

-- ------------------------------------------------------------------------

instance Complement Formula where
  notB :: Formula -> Formula
notB = Uninterned Formula -> Formula
UFormula -> Formula
forall t. Interned t => Uninterned t -> t
intern (UFormula -> Formula)
-> (Formula -> UFormula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> UFormula
UNot

instance MonotoneBoolean Formula where
  andB :: [Formula] -> Formula
andB = Uninterned Formula -> Formula
UFormula -> Formula
forall t. Interned t => Uninterned t -> t
intern (UFormula -> Formula)
-> ([Formula] -> UFormula) -> [Formula] -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Formula] -> UFormula
UAnd
  orB :: [Formula] -> Formula
orB  = Uninterned Formula -> Formula
UFormula -> Formula
forall t. Interned t => Uninterned t -> t
intern (UFormula -> Formula)
-> ([Formula] -> UFormula) -> [Formula] -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Formula] -> UFormula
UOr

instance IfThenElse Formula Formula where
  ite :: Formula -> Formula -> Formula -> Formula
ite Formula
c Formula
t Formula
e = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> Formula -> UFormula
UITE Formula
c Formula
t Formula
e)

instance Boolean Formula where
  .=>. :: Formula -> Formula -> Formula
(.=>.) Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UImply Formula
p Formula
q)
  .<=>. :: Formula -> Formula -> Formula
(.<=>.) Formula
p Formula
q = Uninterned Formula -> Formula
forall t. Interned t => Uninterned t -> t
intern (Formula -> Formula -> UFormula
UEquiv Formula
p Formula
q)

-- ------------------------------------------------------------------------

fold :: Boolean b => (SAT.Lit -> b) -> Formula -> b
fold :: forall b. Boolean b => (Lit -> b) -> Formula -> b
fold Lit -> b
f Formula
formula = (forall s. ST s b) -> b
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s b) -> b) -> (forall s. ST s b) -> b
forall a b. (a -> b) -> a -> b
$ do
  HashTable s Formula b
h <- Lit -> ST s (HashTable s Formula b)
forall s k v. Lit -> ST s (HashTable s k v)
C.newSized Lit
256
  let g :: Formula -> ST s b
g Formula
x = do
        Maybe b
m <- HashTable s Formula b -> Formula -> ST s (Maybe b)
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s Formula b
h Formula
x
        case Maybe b
m of
          Just b
y -> b -> ST s b
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return b
y
          Maybe b
Nothing -> do
            b
y <-
              case Formula
x of
                Atom Lit
lit -> b -> ST s b
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> b
f Lit
lit)
                And [Formula]
ps -> [b] -> b
forall a. MonotoneBoolean a => [a] -> a
andB ([b] -> b) -> ST s [b] -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Formula -> ST s b) -> [Formula] -> ST s [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Formula -> ST s b
g [Formula]
ps
                Or [Formula]
ps -> [b] -> b
forall a. MonotoneBoolean a => [a] -> a
orB ([b] -> b) -> ST s [b] -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Formula -> ST s b) -> [Formula] -> ST s [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Formula -> ST s b
g [Formula]
ps
                Not Formula
p -> b -> b
forall a. Complement a => a -> a
notB (b -> b) -> ST s b -> ST s b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p
                Imply Formula
p Formula
q -> b -> b -> b
forall a. Boolean a => a -> a -> a
(.=>.) (b -> b -> b) -> ST s b -> ST s (b -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p ST s (b -> b) -> ST s b -> ST s b
forall a b. ST s (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
q
                Equiv Formula
p Formula
q -> b -> b -> b
forall a. Boolean a => a -> a -> a
(.<=>.) (b -> b -> b) -> ST s b -> ST s (b -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p ST s (b -> b) -> ST s b -> ST s b
forall a b. ST s (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
q
                ITE Formula
p Formula
q Formula
r -> b -> b -> b -> b
forall b a. IfThenElse b a => b -> a -> a -> a
ite (b -> b -> b -> b) -> ST s b -> ST s (b -> b -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula -> ST s b
g Formula
p ST s (b -> b -> b) -> ST s b -> ST s (b -> b)
forall a b. ST s (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
q ST s (b -> b) -> ST s b -> ST s b
forall a b. ST s (a -> b) -> ST s a -> ST s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> ST s b
g Formula
r
            HashTable s Formula b -> Formula -> b -> ST s ()
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s Formula b
h Formula
x b
y
            b -> ST s b
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return b
y
  Formula -> ST s b
g Formula
formula

evalFormula :: SAT.IModel m => m -> Formula -> Bool
evalFormula :: forall m. IModel m => m -> Formula -> Bool
evalFormula m
m = (Lit -> Bool) -> Formula -> Bool
forall b. Boolean b => (Lit -> b) -> Formula -> b
fold (m -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalLit m
m)

toBoolExpr :: Formula -> BoolExpr.BoolExpr SAT.Lit
toBoolExpr :: Formula -> BoolExpr Lit
toBoolExpr = (Lit -> BoolExpr Lit) -> Formula -> BoolExpr Lit
forall b. Boolean b => (Lit -> b) -> Formula -> b
fold Lit -> BoolExpr Lit
forall a. a -> BoolExpr a
BoolExpr.Atom

fromBoolExpr :: BoolExpr.BoolExpr SAT.Lit -> Formula
fromBoolExpr :: BoolExpr Lit -> Formula
fromBoolExpr = (Lit -> Formula) -> BoolExpr Lit -> Formula
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Lit -> Formula
Atom

-- ------------------------------------------------------------------------

simplify :: Formula -> Formula
simplify :: Formula -> Formula
simplify = Simplify -> Formula
runSimplify (Simplify -> Formula)
-> (Formula -> Simplify) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lit -> Simplify) -> Formula -> Simplify
forall b. Boolean b => (Lit -> b) -> Formula -> b
fold (Formula -> Simplify
Simplify (Formula -> Simplify) -> (Lit -> Formula) -> Lit -> Simplify
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lit -> Formula
Atom)

newtype Simplify = Simplify{ Simplify -> Formula
runSimplify :: Formula }

instance Complement Simplify where
  notB :: Simplify -> Simplify
notB (Simplify (Not Formula
x)) = Formula -> Simplify
Simplify Formula
x
  notB (Simplify Formula
x) = Formula -> Simplify
Simplify (Formula -> Formula
Not Formula
x)

instance MonotoneBoolean (Simplify) where
  orB :: [Simplify] -> Simplify
orB [Simplify]
xs
    | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Formula -> Bool
isTrue [Formula]
ys = Formula -> Simplify
Simplify Formula
forall a. MonotoneBoolean a => a
true
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula -> Simplify) -> Formula -> Simplify
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
Or [Formula]
ys
    where
      ys :: [Formula]
ys = [[Formula]] -> [Formula]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Formula -> [Formula]
f Formula
x | Simplify Formula
x <- [Simplify]
xs]
      f :: Formula -> [Formula]
f (Or [Formula]
zs) = [Formula]
zs
      f Formula
z = [Formula
z]
  andB :: [Simplify] -> Simplify
andB [Simplify]
xs
    | (Formula -> Bool) -> [Formula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Formula -> Bool
isFalse [Formula]
ys = Formula -> Simplify
Simplify Formula
forall a. MonotoneBoolean a => a
false
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula -> Simplify) -> Formula -> Simplify
forall a b. (a -> b) -> a -> b
$ [Formula] -> Formula
And [Formula]
ys
    where
      ys :: [Formula]
ys = [[Formula]] -> [Formula]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Formula -> [Formula]
f Formula
x | Simplify Formula
x <- [Simplify]
xs]
      f :: Formula -> [Formula]
f (And [Formula]
zs) = [Formula]
zs
      f Formula
z = [Formula
z]

instance IfThenElse Simplify Simplify where
  ite :: Simplify -> Simplify -> Simplify -> Simplify
ite (Simplify Formula
c) (Simplify Formula
t) (Simplify Formula
e)
    | Formula -> Bool
isTrue Formula
c  = Formula -> Simplify
Simplify Formula
t
    | Formula -> Bool
isFalse Formula
c = Formula -> Simplify
Simplify Formula
e
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula -> Formula -> Formula -> Formula
ITE Formula
c Formula
t Formula
e)

instance Boolean Simplify where
  Simplify Formula
x .=>. :: Simplify -> Simplify -> Simplify
.=>. Simplify Formula
y
    | Formula -> Bool
isFalse Formula
x = Simplify
forall a. MonotoneBoolean a => a
true
    | Formula -> Bool
isTrue Formula
y  = Simplify
forall a. MonotoneBoolean a => a
true
    | Formula -> Bool
isTrue Formula
x  = Formula -> Simplify
Simplify Formula
y
    | Formula -> Bool
isFalse Formula
y = Simplify -> Simplify
forall a. Complement a => a -> a
notB (Formula -> Simplify
Simplify Formula
x)
    | Bool
otherwise = Formula -> Simplify
Simplify (Formula
x Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Formula
y)

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

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

-- ------------------------------------------------------------------------

newtype JSON = JSON{ JSON -> Value
getJSON :: J.Value }

instance Complement JSON where
  notB :: JSON -> JSON
notB (JSON Value
x) = Value -> JSON
JSON (Value -> JSON) -> Value -> JSON
forall a b. (a -> b) -> a -> b
$ Value -> Value
jNot Value
x

instance MonotoneBoolean JSON where
  andB :: [JSON] -> JSON
andB [JSON]
xs = Value -> JSON
JSON (Value -> JSON) -> Value -> JSON
forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"operator" :: J.Value)
    , Key
"name" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"and" :: J.Value)
    , Key
"operands" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Value
x | JSON Value
x <- [JSON]
xs]
    ]
  orB :: [JSON] -> JSON
orB [JSON]
xs = Value -> JSON
JSON (Value -> JSON) -> Value -> JSON
forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"operator" :: J.Value)
    , Key
"name" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"or" :: J.Value)
    , Key
"operands" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Value
x | JSON Value
x <- [JSON]
xs]
    ]

instance IfThenElse JSON JSON where
  ite :: JSON -> JSON -> JSON -> JSON
ite (JSON Value
c) (JSON Value
t) (JSON Value
e) = Value -> JSON
JSON (Value -> JSON) -> Value -> JSON
forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"operator" :: J.Value)
    , Key
"name" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"ite" :: J.Value)
    , Key
"operands" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Value
c, Value
t, Value
e]
    ]

instance Boolean JSON where
  .=>. :: JSON -> JSON -> JSON
(.=>.) (JSON Value
p) (JSON Value
q) = Value -> JSON
JSON (Value -> JSON) -> Value -> JSON
forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"operator" :: J.Value)
    , Key
"name" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"=>" :: J.Value)
    , Key
"operands" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Value
p, Value
q]
    ]
  .<=>. :: JSON -> JSON -> JSON
(.<=>.) (JSON Value
p) (JSON Value
q) = Value -> JSON
JSON (Value -> JSON) -> Value -> JSON
forall a b. (a -> b) -> a -> b
$ [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"operator" :: J.Value)
    , Key
"name" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"<=>" :: J.Value)
    , Key
"operands" Key -> [Value] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Value
p, Value
q]
    ]

instance J.ToJSON Formula where
  toJSON :: Formula -> Value
toJSON = JSON -> Value
getJSON (JSON -> Value) -> (Formula -> JSON) -> Formula -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lit -> JSON) -> Formula -> JSON
forall b. Boolean b => (Lit -> b) -> Formula -> b
fold (Value -> JSON
JSON (Value -> JSON) -> (Lit -> Value) -> Lit -> JSON
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lit -> Value
jLit)

instance J.FromJSON Formula where
  parseJSON :: Value -> Parser Formula
parseJSON Value
x = [Parser Formula] -> Parser Formula
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
    [ Lit -> Formula
Atom (Lit -> Formula) -> Parser Lit -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Lit
parseVar Value
x
    , (Value -> Parser Formula) -> Value -> Parser Formula
forall a. (Value -> Parser a) -> Value -> Parser a
withNot (\Value
y -> Formula -> Formula
Not (Formula -> Formula) -> Parser Formula -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
y) Value
x
    , ([Value] -> Parser Formula) -> Value -> Parser Formula
forall a. ([Value] -> Parser a) -> Value -> Parser a
withAnd (\[Value]
xs -> [Formula] -> Formula
And ([Formula] -> Formula) -> Parser [Formula] -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Parser Formula) -> [Value] -> Parser [Formula]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON [Value]
xs) Value
x
    , ([Value] -> Parser Formula) -> Value -> Parser Formula
forall a. ([Value] -> Parser a) -> Value -> Parser a
withOr (\[Value]
xs -> [Formula] -> Formula
Or ([Formula] -> Formula) -> Parser [Formula] -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Parser Formula) -> [Value] -> Parser [Formula]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON [Value]
xs) Value
x
    , (Value -> Value -> Value -> Parser Formula)
-> Value -> Parser Formula
forall a.
(Value -> Value -> Value -> Parser a) -> Value -> Parser a
withITE (\Value
c Value
t Value
e -> Formula -> Formula -> Formula -> Formula
ITE (Formula -> Formula -> Formula -> Formula)
-> Parser Formula -> Parser (Formula -> Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
c Parser (Formula -> Formula -> Formula)
-> Parser Formula -> Parser (Formula -> Formula)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
t Parser (Formula -> Formula) -> Parser Formula -> Parser Formula
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
e) Value
x
    , (Value -> Value -> Parser Formula) -> Value -> Parser Formula
forall a. (Value -> Value -> Parser a) -> Value -> Parser a
withImply (\Value
a Value
b -> Formula -> Formula -> Formula
Imply (Formula -> Formula -> Formula)
-> Parser Formula -> Parser (Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
a Parser (Formula -> Formula) -> Parser Formula -> Parser Formula
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
b) Value
x
    , (Value -> Value -> Parser Formula) -> Value -> Parser Formula
forall a. (Value -> Value -> Parser a) -> Value -> Parser a
withEquiv (\Value
a Value
b -> Formula -> Formula -> Formula
Equiv (Formula -> Formula -> Formula)
-> Parser Formula -> Parser (Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
a Parser (Formula -> Formula) -> Parser Formula -> Parser Formula
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Value -> Parser Formula
forall a. FromJSON a => Value -> Parser a
J.parseJSON Value
b) Value
x
    ]

-- ------------------------------------------------------------------------