-- |Do satisfiability computations on any FirstOrderFormula formula by
-- converting it to a convenient instance of PropositionalFormula and
-- using the satisfiable function from that instance.  Currently we
-- use the satisfiable function from the PropLogic package, by the
-- Bucephalus project.
{-# LANGUAGE FlexibleContexts, OverloadedStrings, RankNTypes, ScopedTypeVariables #-}
module Data.Logic.Satisfiable
    ( satisfiable
    , theorem
    , inconsistant
    , invalid
    ) where

import Data.Logic.Classes.Atom (Atom)
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), toPropositional)
import Data.Logic.Classes.Literal.Literal (Literal)
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Propositional (PropositionalFormula)
import Data.Logic.Classes.Term (Term)
import Data.Logic.Harrison.Skolem (SkolemT)
import Data.Logic.Instances.PropLogic ()
import Data.Logic.Normal.Clause (clauseNormalForm)
import qualified Data.Set as Set (Set, toList)
import qualified PropLogic as PL (PropAlg(satisfiable), PropForm(A, CJ, DJ))

-- |Is there any variable assignment that makes the formula true?
-- satisfiable :: forall formula atom term v f m. (Monad m, FirstOrderFormula formula atom v, Formula atom term v, Term term v f, Ord formula, Literal formula atom v, Ord atom) =>
--                 formula -> SkolemT v term m Bool
satisfiable :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v,
                                                Ord atom, Monad m, Eq formula, Ord formula) =>
               formula -> SkolemT v term m Bool
satisfiable f =
    do (clauses :: Set.Set (Set.Set formula)) <- clauseNormalForm f
       let f' = PL.CJ . map (PL.DJ . map (toPropositional PL.A)) . map Set.toList . Set.toList $ clauses
       return . PL.satisfiable $ f'

-- |Is the formula always false?  (Not satisfiable.)
inconsistant :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v,
                                                 Ord atom, Monad m, Eq formula, Ord formula) =>
                formula -> SkolemT v term m Bool
inconsistant f =  satisfiable f >>= return . not

-- |Is the negation of the formula inconsistant?
theorem :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v,
                                            Ord atom, Monad m, Eq formula, Ord formula) =>
           formula -> SkolemT v term m Bool
theorem f = inconsistant ((.~.) f)

-- |A formula is invalid if it is neither a theorem nor inconsistent.
invalid :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v,
                                            Ord atom, Monad m, Eq formula, Ord formula) =>
           formula -> SkolemT v term m Bool
invalid f = inconsistant f >>= \ fi -> theorem f >>= \ ft -> return (not (fi || ft))