content: {- |
  Module      :  $EmptyHeader$
  Description :  <optional short description entry>
  Copyright   :  (c) <Authors or Affiliations>
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  <email>
  Stability   :  unstable | experimental | provisional | stable | frozen
  Portability :  portable | non-portable (<reason>)
  
  <optional description>
  -}
  module GenericSequent where
  
  import ModalLogic
  import CombLogic
  import Data.List as List
  -- import Data.Map as Map
  
  -- | Generate all possible clauses out of a list of atoms
  allClauses :: [a] -> [Clause a]
  allClauses x = case x of
                   h : t -> let addPositive c (Implies n p) = Implies n (c : p)
                                addNegative c (Implies n p) = Implies (c : n) p
                          in List.map (addPositive h) (allClauses t) ++
                             List.map (addNegative h) (allClauses t)
                   _ -> [Implies [] []]
  
  -- | Extract the modal atoms from a formula
  getMA :: Eq a => Boole a -> [Boole a]
  getMA x = case x of
              And phi psi -> getMA phi `List.union` getMA psi
              Not phi -> getMA phi
              At phi -> [At phi]
              _ -> []
  
  -- | Substitution of modal atoms within a "Boole" expression
  subst :: Eq a => Boole a -> Clause (Boole a) -> Boole a
  subst x s@(Implies neg pos) =
    case x of
      And phi psi -> And (subst phi s) (subst psi s)
      Not phi -> Not (subst phi s)
      T -> T
      F -> F
      _ | elem x neg -> F
      _ | elem x pos -> T
      _ -> error "GenericSequent.subst"
  
  -- | Evaluation of an instantiated "Boole" expression
  eval :: Boole a -> Bool
  eval x = case x of
             And phi psi -> eval phi && eval psi
             Not phi -> not (eval phi)
             T -> True
             F -> False
             _ -> error "GenericSequent.eval"
  
  -- | DNF: disjunctive normal form of a Boole expression
  dnf :: (Eq a) => Boole a -> [Clause (Boole a)]
  dnf phi = List.filter (eval . subst phi) (allClauses (getMA phi))
  
  -- | CNF: conjunctive normal form of a Boole expression
  cnf :: (Eq a) => Boole a -> [Clause (Boole a)]
  cnf phi = List.map (\ (Implies x y) -> Implies y x) (dnf (Not phi))
  
  -- | Generic Provability Function
  provable :: (Eq a, Form a b c) => Boole a -> Bool
  provable _ = True
  {-
  provable phi =
    let unwrap (Subst x) = Map.elems x
    in all (\c -> any (all provable) (List.map unwrap.snd (match c))) (cnf phi)
  -}
  
  -- | Generic Satisfiability Function
  sat :: (Eq a, Form a b c) => Boole a -> Bool
  sat phi = not $ provable $ neg phi
  
  -- | Function for "normalizing" negation
  neg :: Eq a => Boole a -> Boole a
  neg phi = case phi of
              Not psi -> psi
              _ -> phi
  