{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- |
-- Module      : AutoProof.Internal.Classical.SAT.TruthAssignment
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Defines the TruthAssignment class.
module AutoProof.Internal.Classical.SAT.TruthAssignment
  ( TruthAssignment (evalVar, evalFormula),
    (|=),
  )
where

import AutoProof.Internal.Formula
  ( Formula
      ( And,
        Iff,
        Imp,
        Lit,
        Not,
        Or,
        Var
      ),
  )
import Data.Map (Map)
import qualified Data.Map as Map

-- | Class representing truth assignments for evalutating propositional logic
-- formulas.
class TruthAssignment t a where
  -- | Evaluate the truth value of a variable under a given truth assignment.
  evalVar :: t -> a -> Bool

  -- | Evaluate the truth value of a formula under a given truth assignment.
  evalFormula :: t -> Formula a -> Bool
  evalFormula _ (Lit b :: Bool
b) = Bool
b
  evalFormula t :: t
t (Var x :: a
x) = t -> a -> Bool
forall t a. TruthAssignment t a => t -> a -> Bool
evalVar t
t a
x
  evalFormula t :: t
t (Not a :: Formula a
a) = Bool -> Bool
not (t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t Formula a
a)
  evalFormula t :: t
t (Imp a :: Formula a
a b :: Formula a
b) = Bool -> Bool
not (t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t Formula a
a) Bool -> Bool -> Bool
|| t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t Formula a
b
  evalFormula t :: t
t (Or a :: Formula a
a b :: Formula a
b) = t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t Formula a
a Bool -> Bool -> Bool
|| t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t Formula a
b
  evalFormula t :: t
t (And a :: Formula a
a b :: Formula a
b) = t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t Formula a
a Bool -> Bool -> Bool
&& t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t Formula a
b
  evalFormula t :: t
t (Iff a :: Formula a
a b :: Formula a
b) = t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula t
t (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
a Formula a
b) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
b Formula a
a))

-- | Semantic entailment relation. This is an infix alias of 'evalFormula'.
--
-- ==== __Examples__
--
-- >>> t = Map.fromList $ [("a", True), ("b", False)]
-- >>> t |= And (Var "a") (Not (Var "b"))
-- True
(|=) :: TruthAssignment t a => t -> Formula a -> Bool
|= :: t -> Formula a -> Bool
(|=) = t -> Formula a -> Bool
forall t a. TruthAssignment t a => t -> Formula a -> Bool
evalFormula

infix 5 |=

-- | Truth assignments where a missing key in the map is interpreted as 'False'.
--
-- ==== __Examples__
--
-- >>> t = Map.fromList $ [("a", True), ("b", False)]
-- >>> t |= And (Var "a") (Not (Var "b"))
-- True
--
-- >>> t = Map.fromList $ [("a", True)]
-- >>> t |= Imp (Var "a") (Var "b")
-- False
instance Ord a => TruthAssignment (Map a Bool) a where
  evalVar :: Map a Bool -> a -> Bool
evalVar t :: Map a Bool
t x :: a
x = Bool -> a -> Map a Bool -> Bool
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Bool
False a
x Map a Bool
t

-- | Assigns all propositional variables the truth value 'False'. Can be used to
-- evaluate closed formulas.
--
-- ==== __Examples__
--
-- >>> () |= (Var "a")
-- False
--
-- >>> () |= (Or (Lit True) (Lit False))
-- True
instance TruthAssignment () a where
  evalVar :: () -> a -> Bool
evalVar () = Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
False