{-# LANGUAGE FlexibleInstances #-}
import Prelude hiding (and,or,not)
import qualified Prelude as P (and,or,not) 
import qualified Data.Set as Set

class Prop a where
  p :: Int -> a
class SentConn a where
  and :: a -> a -> a
  or :: a -> a -> a
  not :: a -> a
implies :: SentConn a => a -> a -> a
a `implies` b = not a `or` b

data Sequent a = [a] :- a deriving (Eq,Show,Ord)


-- |
-- @'mkConjunction'@ takes a non-empty list of formulae and creates their
-- conjunction.  The non-empty list argument is formally received as the
-- head of the list (the first argument) and the tail (the second
-- argument).
--
-- @
-- mkConjunction phi0 [phi1,phi2,phi3] = phi1 `and` phi2 `and` phi3 `and` phi0
-- @
-- 
mkConjunction :: SentConn a => a -> [a] -> a
mkConjunction = foldr and


-- |
-- @'sequentToTerm'@ takes a sequent of the form @A :- phi@ and turns it
-- into a formula of the form @A `implies` phi@ (but where @A@ has been
-- turned from a list into a big conjunction).
-- 
-- A sequent @A :- phi@ is intended to assert that whenever all formulae
-- in @A@ are true in a situation, @phi@ is true in that situation as
-- well.  This is mirrored by the implication @A `implies` phi@, which is
-- true in a situation when @phi@ is true if @A@ is.
--
sequentToTerm :: SentConn a => Sequent a -> a
sequentToTerm ([] :- cons) = cons
sequentToTerm ((b:bs) :- cons) = mkConjunction b bs `implies` cons

-- |
-- = Type 'Signed' and associated functions
--
-- == Type 'Signed'
--
-- The type @'Signed' a@ is a wrapper for a pair @(Bool,a)@.  It is
-- intended as an implementation of the signed tableau formula
-- \(\textbf{S}:\phi\).
--
-- == Projections
--
-- 'dropSign' and 'isTrueSign' act as projection functions, mapping a
-- pair of type @(Bool,a)@ to the underlying @a@ and @Bool@
-- respectively.
--
-- == Creating and modifying
--
-- 'mkSign' is simply a curried version of the constructor for type @'Signed'@:
--
-- @
-- 'mkSign' = curry 'Signed'
-- @
--
-- 'flipSign' negates the underlying boolean in a sign.
--
newtype Signed a = Signed {unSigned :: (Bool,a)} deriving (Eq,Ord)
dropSign :: Signed a -> a
dropSign = snd . unSigned
isTrueSign :: Signed a -> Bool
isTrueSign = fst . unSigned
mkSign :: Bool -> a -> Signed a
mkSign b a = Signed (b,a)
flipSign :: Signed a -> Signed a
flipSign (Signed (b,a)) = mkSign (P.not b) a
instance Show a => Show (Signed a) where
  show (Signed (b,a)) = (if b then "T:" else "F:") ++ show a

-- |
-- = Type 'Branch' and associated functions
--
-- == Type 'Branch'
--
-- The type @'Branch' a@ is a set of objects of type @'Sign' a@.  It
-- represents a branch of a tableau.
--
-- An @'emptyBranch'@ is the empty set.
--
-- == Testing branches
--
-- The function 'closes' tests whether the negated counterpart of a
-- particular object is already contained in the branch.  If it is,
-- the branch is closed, and the function returns @True@.
--
-- == Modifying branches
--
-- The function 'addToBranch' is a wrapper for the insertion operation
-- of the underlying set.
--
-- The function 'filterBranch' is a wrapper for the filter operation
-- of the underlying set.
--
-- == Branches and models
--
-- Each 'Branch' represents the set of valuations each of which
-- assigns the truth value to atomic formulae indicated by the signs
-- associated with integers.  Integers not appearing in the branch may
-- be associated with any truth value.  The valuations which a given
-- branch represents, form a boolean lattice: the powerset of the
-- atomic propositions not mentioned in the branch.  There are two
-- elements of this lattice which are structurally distinguishable:
-- the top element, which contains all atomic propositions not
-- mentioned in the branch, and the bottom element, containing none of
-- them.  These correspond to the valuation which makes all atomic
-- propositions not mentioned in the branch true, and the valuation
-- which makes all atomic propositions not mentioned in the branch
-- false, respectively.  We can think of these two valuations as
-- emerging from the branch by either having a default assumption that
-- everything is true, unless the branch says otherwise, or that
-- everything is false, unless the branch says otherwise.  This latter
-- assumption is popular in artificial intelligence, where the model
-- satisfying it is called the /minimal model/.  Every branch can be
-- identified with its minimal model, at the cost of losing
-- information about which propositions *must* be false, and which
-- merely *may* be false.  If we only are interested in minimal
-- models, we can replace each branch with the set of atomic
-- propositions which must be true.  This is done by the function
-- 'mkMinModel'.
--
-- == Visualising Branches
--
-- The default "Show" instance for a 'Branch' simply turns it into a
-- list.  We can call instead 'showMinModel' which first constructs
-- the minimal model for the branch before showing it.  However, if
-- all atoms are true, it is redundant to show as well the sign, so
-- 'showMinModel' strips off the sign before showing the branch.
--
newtype Branch a = Branch {unBranch :: Set.Set (Signed a)} deriving (Eq,Ord)
emptyBranch :: Branch a
emptyBranch = Branch Set.empty
closes :: Ord a => Signed a -> Branch a -> Bool
closes sg = Set.member (flipSign sg) . unBranch
addToBranch :: Ord a => Signed a -> Branch a -> Branch a
addToBranch sg = Branch . Set.insert sg . unBranch
filterBranch :: (Signed a -> Bool) -> Branch a -> Branch a
filterBranch p = Branch . Set.filter p . unBranch
mkMinModel :: Ord a => Branch a -> Branch a
mkMinModel = filterBranch isTrueSign
instance Show a => Show (Branch a) where
  show = show . Set.toList . unBranch
showMinModel :: (Ord a, Show a) => Branch a -> String  
showMinModel = show . fmap dropSign . Set.toList . unBranch . mkMinModel

-- |
-- = Type 'Tableau' and associated functions
--
-- == Type 'Tableau'
--
-- The type @'Tableau a'@ is a set of branches, and represents an
-- entire tableau.
--
-- An @'emptyTableau'@ is the empty set.
--
-- A @'blankTableau'@ is the tableau containing just the @'emptyBranch'@.
--
-- == Creating and modifying tableaux
--
-- === Monadic operations
--
-- Sets form a monad, modulo the type class constraints on the operations.
--
--   [@fmap@]: The functorial behaviour on arrows is given by the
--   @'mapTableau'@ function, which is a wrapper for the map operation
--   in the "Set" module.
--
--   [@return@]: The monadic return operation is given by the function
--   @'oneBranchTableau'@, which is a wrapper for the singleton
--   operation in the "Set" module.
--
--   [@bind@]: The monadic bind operation is given by the function
--   @'bindTableau'@, which works by taking the union of the results
--   of applying the input function to each branch in the input
--   tableau.
--
-- ==== Monad Plus operations
--
-- Sets form a richer kind of monad, supporting (non-deterministic)
-- /choice/ and /failure/.
--
--    [@mzero@]: The failure value is the @'emptyTableau'@, which is a
--    wrapper for the empty set
--
--    [@mplus@]: The choice operation is @'combineTableau'@, which is
--    a wrapper for the union operation on the underlying sets
--
-- == Visualizing Tableaux
--
-- The default visualization for Tableaux is as a list of shown branches.
--
newtype Tableau a = Tableau {unTableau :: Set.Set (Branch a)} deriving (Eq,Ord)
emptyTableau :: Tableau a
emptyTableau = Tableau Set.empty
oneBranchTableau :: Branch a -> Tableau a
oneBranchTableau = Tableau . Set.singleton 
blankTableau :: Tableau a
blankTableau = oneBranchTableau emptyBranch
combineTableaux :: Ord a => Tableau a -> Tableau a -> Tableau a
combineTableaux (Tableau t1) (Tableau t2) = Tableau (t1 `Set.union` t2)
mapTableau :: Ord b => (Branch a -> Branch b) -> Tableau a -> Tableau b
mapTableau f = Tableau . Set.map f . unTableau
bindTableau :: Ord b => Tableau a -> (Branch a -> Tableau b) -> Tableau b
bindTableau tbl f  = Tableau $ Set.foldr (Set.union . unTableau . f) Set.empty $ unTableau tbl
instance (Show a, Ord a) => Show (Tableau a) where
  show = show . Set.toList . unTableau
showMinTableau :: (Show a, Ord a) => Tableau a -> String
showMinTableau =  unlines . Set.toList . Set.map showMinModel . unTableau

-- |
-- = 'BranchToTableau' and associated functions
--
-- A @'BranchToTableau' a@ is a function from a @'Branch' a@ to a
-- @'Tableau' a@.  Both input and output are morally monadic, and so
-- it is roughly of type @m a -> m (m a)@.  Indeed, both are a
-- @MonadPlus@, and so they have in particular a @mzero@ object.
--
-- Given a @'BranchToTableau' a@, the @mzero@ object of type @'Branch'
-- a@ allows us to obtain a @'Tableau' a@.  This is what
-- 'constructTableau' does:
--
-- @
-- constructTableau :: MonadPlus m => (m a -> m (m a)) -> m (m a)
-- constructTableau f = f mzero
-- @
--
-- == Combining objects of type 'BranchToTableau'
--
-- We can combine functions of type 'BranchToTableau' either in a
-- serial way, or in a parallel way.  'serialComposition' is done via
-- 'bindTableau', and 'parallelComposition' via 'combineTableaux'.
--
-- The identity element for 'serialComposition' is
-- 'idBranchToTableau'.  It is just a wrapper for the monadic @return@
-- of the 'Tableau' type.
--
newtype BranchToTableau a = BranchToTableau {unBranchToTableau :: Branch a -> Tableau a}
constructTableau :: BranchToTableau a -> Tableau a
constructTableau (BranchToTableau phi) = phi emptyBranch

idBranchToTableau :: BranchToTableau a
idBranchToTableau = BranchToTableau oneBranchTableau

serialComposition :: Ord a => BranchToTableau a -> BranchToTableau a -> BranchToTableau a
serialComposition (BranchToTableau f) (BranchToTableau g) = BranchToTableau (\b -> g b `bindTableau` f)

parallelComposition :: (Eq a, Ord a) => BranchToTableau a -> BranchToTableau a -> BranchToTableau a
parallelComposition (BranchToTableau f) (BranchToTableau g) = BranchToTableau (\b -> f b `combineTableaux` g b)


-- |
-- = 'Formula' and associated functions
--
-- A 'Formula' is a wrapper for a function from a boolean to a
-- 'BranchToTableau'.  A basic element of this type is the constant
-- function from booleans to the identity element of
-- 'BranchToTableau'.  We call this element 'idFormula'.
--
-- As we will mostly work with signed formulae, @'Signed' ('Formula'
-- a)@, we define a function for feeding the boolean sign to the
-- formula it tags: 'unSignedFormula'.
--
-- The 'alpha' and 'beta' type 'Signed' 'Formula' require specifying
-- two sub-signed formulae (typically named either @alpha1@ and
-- @alpha2@ or @beta1@ and @beta2@).  Once this is done, an 'alpha'
-- type 'Signed' 'Formula' will let both of these sub-formulae operate
-- serially on a branch, and the 'beta' type will let both operate in
-- parallel on a branch.
--
-- == Instances of 'Prop' and 'SentConn'
--
-- 'Formula' can be made into an instance of 'Prop' and of 'SentConn'.
--
-- === 'Formula' is an instance of 'Prop'
--
-- A proposition @'p' i@ can be construed as a @'Formula' Int' by
-- having it, given a boolean sign and a branch, test whether the
-- signed atom would close the branch.  If it does, we return the
-- 'emptyTableau'.  Otherwise, we add the signed atom to the branch.
--
-- === 'Formula' is an instance of 'SentConn'
--
-- Of practical interest for us is that the sentential connectives can
-- be interpreted as functions from booleans to functions from
-- branches to tableaux.
--
-- The role of the boolean is two-fold.  First, negation flips the
-- boolean.  Second, the boolean sign is used as a test to determine
-- whether we interpret a connective in an alpha or in a beta way.
--
-- Using the 'idFormula', we can interpret 'not' as an 'alpha' formula
-- without the associated computational redundancy.
--
-- == Constructing Countermodels
--
-- The tableau method attempts to construct a situation compatible
-- with an initial assignment of truth or falsity to a formula.
-- 'makeFormula' takes a boolean and a formula, and constructs a
-- tableau which attempts to construct situations in which that
-- formula receives the input truth value.  A counter model for a
-- formula is one which makes the formula false.  The function
-- 'counterModels' attempts to make a tableau which makes the input
-- formula false.
-- 
newtype Formula a = Formula {unFormula :: Bool -> BranchToTableau a}
idFormula :: Formula a
idFormula = Formula $ const idBranchToTableau
unSignedFormula :: Signed (Formula a) -> BranchToTableau a
unSignedFormula (Signed (sign,Formula phi)) = phi sign
alpha :: Ord a => Signed (Formula a) -> Signed (Formula a) -> BranchToTableau a
alpha alpha1 alpha2 = unSignedFormula alpha1 `serialComposition` unSignedFormula alpha2
beta :: (Eq a,Ord a) => Signed (Formula a) -> Signed (Formula a) -> BranchToTableau a
beta beta1 beta2 = unSignedFormula beta1 `parallelComposition` unSignedFormula beta2

instance Prop (Formula Int) where
  p i = Formula $ \sign ->
    let atom = mkSign sign i
    in
      BranchToTableau $ \branch ->
      if atom `closes` branch
      then emptyTableau
      else oneBranchTableau $ addToBranch atom branch

instance (Eq a,Ord a) => SentConn (Formula a) where
  not phi = Formula $ \b ->
    alpha (mkSign (P.not b) phi) (mkSign b idFormula)
  and phi psi = Formula $ \b ->
    (if b then alpha else beta) (mkSign b phi)
                                (mkSign b psi)
  or phi psi = Formula $ \b ->
    (if b then beta else alpha) (mkSign b phi)
                                (mkSign b psi)

makeFormula :: Bool -> Formula Int -> Tableau Int
makeFormula b = constructTableau . unSignedFormula . mkSign b

counterModel :: Formula Int -> Tableau Int
counterModel = makeFormula False