-- | Classical propositional formulas and evaluation.
--
-- The formula AST is the \"syntax\"; @Bool@ (and other Boolean carriers)
-- are compile targets for @evalProp@.
module Circuit.Logics.Prop
  ( Prop (..),
    evalProp,
    evalPropH3,
    simplify,
  )
where

import Circuit.Logics.Boolean (Complemented (..))
import Circuit.Logics.H3 (H3 (..))
import Circuit.Logics.Heyting (Heyting (..))
import Circuit.Logics.Lattice
  ( JoinSemiLattice (..),
    LowerBounded (..),
    MeetSemiLattice (..),
    UpperBounded (..),
    (/\),
    (\/),
  )

-- | Propositional formula over variable names @v@.
data Prop v
  = -- | Atomic variable.
    Var v
  | -- | Falsehood.
    Bot
  | -- | Truth.
    Top
  | -- | Negation.
    Not (Prop v)
  | -- | Conjunction.
    And (Prop v) (Prop v)
  | -- | Disjunction.
    Or (Prop v) (Prop v)
  | -- | Implication.
    Imp (Prop v) (Prop v)
  deriving (Prop v -> Prop v -> Bool
(Prop v -> Prop v -> Bool)
-> (Prop v -> Prop v -> Bool) -> Eq (Prop v)
forall v. Eq v => Prop v -> Prop v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => Prop v -> Prop v -> Bool
== :: Prop v -> Prop v -> Bool
$c/= :: forall v. Eq v => Prop v -> Prop v -> Bool
/= :: Prop v -> Prop v -> Bool
Eq, Eq (Prop v)
Eq (Prop v) =>
(Prop v -> Prop v -> Ordering)
-> (Prop v -> Prop v -> Bool)
-> (Prop v -> Prop v -> Bool)
-> (Prop v -> Prop v -> Bool)
-> (Prop v -> Prop v -> Bool)
-> (Prop v -> Prop v -> Prop v)
-> (Prop v -> Prop v -> Prop v)
-> Ord (Prop v)
Prop v -> Prop v -> Bool
Prop v -> Prop v -> Ordering
Prop v -> Prop v -> Prop v
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 v. Ord v => Eq (Prop v)
forall v. Ord v => Prop v -> Prop v -> Bool
forall v. Ord v => Prop v -> Prop v -> Ordering
forall v. Ord v => Prop v -> Prop v -> Prop v
$ccompare :: forall v. Ord v => Prop v -> Prop v -> Ordering
compare :: Prop v -> Prop v -> Ordering
$c< :: forall v. Ord v => Prop v -> Prop v -> Bool
< :: Prop v -> Prop v -> Bool
$c<= :: forall v. Ord v => Prop v -> Prop v -> Bool
<= :: Prop v -> Prop v -> Bool
$c> :: forall v. Ord v => Prop v -> Prop v -> Bool
> :: Prop v -> Prop v -> Bool
$c>= :: forall v. Ord v => Prop v -> Prop v -> Bool
>= :: Prop v -> Prop v -> Bool
$cmax :: forall v. Ord v => Prop v -> Prop v -> Prop v
max :: Prop v -> Prop v -> Prop v
$cmin :: forall v. Ord v => Prop v -> Prop v -> Prop v
min :: Prop v -> Prop v -> Prop v
Ord, Int -> Prop v -> ShowS
[Prop v] -> ShowS
Prop v -> String
(Int -> Prop v -> ShowS)
-> (Prop v -> String) -> ([Prop v] -> ShowS) -> Show (Prop v)
forall v. Show v => Int -> Prop v -> ShowS
forall v. Show v => [Prop v] -> ShowS
forall v. Show v => Prop v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> Prop v -> ShowS
showsPrec :: Int -> Prop v -> ShowS
$cshow :: forall v. Show v => Prop v -> String
show :: Prop v -> String
$cshowList :: forall v. Show v => [Prop v] -> ShowS
showList :: [Prop v] -> ShowS
Show, ReadPrec [Prop v]
ReadPrec (Prop v)
Int -> ReadS (Prop v)
ReadS [Prop v]
(Int -> ReadS (Prop v))
-> ReadS [Prop v]
-> ReadPrec (Prop v)
-> ReadPrec [Prop v]
-> Read (Prop v)
forall v. Read v => ReadPrec [Prop v]
forall v. Read v => ReadPrec (Prop v)
forall v. Read v => Int -> ReadS (Prop v)
forall v. Read v => ReadS [Prop v]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall v. Read v => Int -> ReadS (Prop v)
readsPrec :: Int -> ReadS (Prop v)
$creadList :: forall v. Read v => ReadS [Prop v]
readList :: ReadS [Prop v]
$creadPrec :: forall v. Read v => ReadPrec (Prop v)
readPrec :: ReadPrec (Prop v)
$creadListPrec :: forall v. Read v => ReadPrec [Prop v]
readListPrec :: ReadPrec [Prop v]
Read, (forall a b. (a -> b) -> Prop a -> Prop b)
-> (forall a b. a -> Prop b -> Prop a) -> Functor Prop
forall a b. a -> Prop b -> Prop a
forall a b. (a -> b) -> Prop a -> Prop b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Prop a -> Prop b
fmap :: forall a b. (a -> b) -> Prop a -> Prop b
$c<$ :: forall a b. a -> Prop b -> Prop a
<$ :: forall a b. a -> Prop b -> Prop a
Functor)

-- | Evaluate a formula given a valuation into a complemented Heyting algebra.
evalProp ::
  (Heyting b, Complemented b) =>
  (v -> b) ->
  Prop v ->
  b
evalProp :: forall b v. (Heyting b, Complemented b) => (v -> b) -> Prop v -> b
evalProp v -> b
env = Prop v -> b
go
  where
    go :: Prop v -> b
go (Var v
v) = v -> b
env v
v
    go Prop v
Bot = b
forall a. LowerBounded a => a
bottom
    go Prop v
Top = b
forall a. UpperBounded a => a
top
    go (Not Prop v
p) = b -> b
forall a. Complemented a => a -> a
complement (Prop v -> b
go Prop v
p)
    go (And Prop v
p Prop v
q) = Prop v -> b
go Prop v
p b -> b -> b
forall a. MeetSemiLattice a => a -> a -> a
/\ Prop v -> b
go Prop v
q
    go (Or Prop v
p Prop v
q) = Prop v -> b
go Prop v
p b -> b -> b
forall a. JoinSemiLattice a => a -> a -> a
\/ Prop v -> b
go Prop v
q
    go (Imp Prop v
p Prop v
q) = Prop v -> b
go Prop v
p b -> b -> b
forall a. Heyting a => a -> a -> a
==> Prop v -> b
go Prop v
q

-- | Three-valued eval: atoms may be unknown; connectives use H3 tables.
--
-- @Not@ on H3 uses the Heyting-style pseudo-complement @a ==> HFalse@.
evalPropH3 :: (v -> H3) -> Prop v -> H3
evalPropH3 :: forall v. (v -> H3) -> Prop v -> H3
evalPropH3 v -> H3
env = Prop v -> H3
go
  where
    go :: Prop v -> H3
go (Var v
v) = v -> H3
env v
v
    go Prop v
Bot = H3
HFalse
    go Prop v
Top = H3
HTrue
    go (Not Prop v
p) = Prop v -> H3
go Prop v
p H3 -> H3 -> H3
forall a. Heyting a => a -> a -> a
==> H3
HFalse
    go (And Prop v
p Prop v
q) = Prop v -> H3
go Prop v
p H3 -> H3 -> H3
forall a. MeetSemiLattice a => a -> a -> a
/\ Prop v -> H3
go Prop v
q
    go (Or Prop v
p Prop v
q) = Prop v -> H3
go Prop v
p H3 -> H3 -> H3
forall a. JoinSemiLattice a => a -> a -> a
\/ Prop v -> H3
go Prop v
q
    go (Imp Prop v
p Prop v
q) = Prop v -> H3
go Prop v
p H3 -> H3 -> H3
forall a. Heyting a => a -> a -> a
==> Prop v -> H3
go Prop v
q

-- | Cheap structural simplify (constants only).
simplify :: Prop v -> Prop v
simplify :: forall v. Prop v -> Prop v
simplify = Prop v -> Prop v
forall v. Prop v -> Prop v
go
  where
    go :: Prop v -> Prop v
go (Not Prop v
p) = case Prop v -> Prop v
go Prop v
p of
      Prop v
Bot -> Prop v
forall v. Prop v
Top
      Prop v
Top -> Prop v
forall v. Prop v
Bot
      Not Prop v
q -> Prop v
q
      Prop v
p' -> Prop v -> Prop v
forall v. Prop v -> Prop v
Not Prop v
p'
    go (And Prop v
p Prop v
q) = case (Prop v -> Prop v
go Prop v
p, Prop v -> Prop v
go Prop v
q) of
      (Prop v
Bot, Prop v
_) -> Prop v
forall v. Prop v
Bot
      (Prop v
_, Prop v
Bot) -> Prop v
forall v. Prop v
Bot
      (Prop v
Top, Prop v
q') -> Prop v
q'
      (Prop v
p', Prop v
Top) -> Prop v
p'
      (Prop v
p', Prop v
q') -> Prop v -> Prop v -> Prop v
forall v. Prop v -> Prop v -> Prop v
And Prop v
p' Prop v
q'
    go (Or Prop v
p Prop v
q) = case (Prop v -> Prop v
go Prop v
p, Prop v -> Prop v
go Prop v
q) of
      (Prop v
Top, Prop v
_) -> Prop v
forall v. Prop v
Top
      (Prop v
_, Prop v
Top) -> Prop v
forall v. Prop v
Top
      (Prop v
Bot, Prop v
q') -> Prop v
q'
      (Prop v
p', Prop v
Bot) -> Prop v
p'
      (Prop v
p', Prop v
q') -> Prop v -> Prop v -> Prop v
forall v. Prop v -> Prop v -> Prop v
Or Prop v
p' Prop v
q'
    go (Imp Prop v
p Prop v
q) = case (Prop v -> Prop v
go Prop v
p, Prop v -> Prop v
go Prop v
q) of
      (Prop v
Bot, Prop v
_) -> Prop v
forall v. Prop v
Top
      (Prop v
_, Prop v
Top) -> Prop v
forall v. Prop v
Top
      (Prop v
Top, Prop v
q') -> Prop v
q'
      (Prop v
p', Prop v
Bot) -> Prop v -> Prop v
forall v. Prop v -> Prop v
Not Prop v
p'
      (Prop v
p', Prop v
q') -> Prop v -> Prop v -> Prop v
forall v. Prop v -> Prop v -> Prop v
Imp Prop v
p' Prop v
q'
    go Prop v
p = Prop v
p