{-
  Theorem prover using the Tableaux method

  Pedro Vasconcelos, 2009-2010
  pbv@dcc.fc.up.pt
-}
module Tableaux where

import FOL
import Unify 
import qualified Data.Map as Map
import Data.Maybe 

{- 
   Data.Tree from Haskell's standard library
   Data.Tree.Zipper is based on the rosezipper package
   A "zipper" is a purely-functional idiom for extending an
   inductive type with a single "hole" (i.e. the active node)
 -}
import Data.Tree
import Zipper 

import Control.Monad
import Control.Monad.State


-- a tableau is a tree zipper
-- of formula, attributes pairs
type Tableau = TreeLoc AttrFormula

-- a formula with atributes
data AttrFormula = 
    AttrFormula { formula   :: Formula
                , is_open   :: !Bool  -- True if in an open branch, False if closed
                , use_count :: !Int   -- number of times used
                } 
    deriving (Eq,Show,Read)

-- allow substitutions on atributed formulas 
instance FV AttrFormula where
    fv af = fv (formula af)
    subst s af = af { formula = subst s (formula af) }


-- add atributes to a formula
attr :: Formula -> AttrFormula
attr f = AttrFormula f (f/=FF) 0


-- make an initial tableau with a single formula
newTableau :: Formula -> Tableau
newTableau f = fromTree (Node (attr f) [])



-- a state monad for proofs
-- (most general unifier, new var counter, new skolem counter)
type Proof a = State Status a

data Status = Status { vars :: !Int     -- variable counter
                     , skolems :: !Int  -- Skolem function counter
                     }
              deriving (Eq,Show,Read)

initial_status :: Status
initial_status = Status { vars=0, skolems=0 } 

-- generate a new variable
newVar :: Proof Var
newVar = do n<-gets vars
            modify (\s -> s { vars=n+1 })
            return ("X_"++show n)

-- generate a new skolem term
newSkolem :: [Var] -> Proof Term
newSkolem vs = do k<-gets skolems
                  modify (\s -> s { skolems=k+1 })
                  return (Fun ("c_"++show k)  (map Var vs))

-- count one extra step
-- incrStep :: Proof ()
-- incrStep = modify (\s -> s{ steps=1+steps s})


-- perform tableau expansion on the current node
expand :: Tableau -> Proof Tableau
expand loc 
    = do disj <- expandFormula f
         return (if disj /= [[f]] then
                    modifyTree (append_open (attrs disj) . incr_uses) loc
                else
                    loc)
    where f = formula (rootLabel (tree loc))
          attrs = map (map attr)           -- add default atributes


incr_uses :: Tree AttrFormula -> Tree AttrFormula
incr_uses (Node x ts) = Node x' ts
    where x' = x { use_count = 1+use_count x }


-- append at the end of open branches 
append_open ::  [[AttrFormula]] -> Tree AttrFormula -> Tree AttrFormula
append_open disj t 
    | not (is_open (rootLabel t)) = t
append_open disj (Node f ts) 
    | null ts   = Node f (fromDisj disj)
    | otherwise = Node f (map (append_open disj) ts)
          
fromDisj :: [[a]] -> Forest a
fromDisj [[p],[q]] = [Node p [], Node q []]
fromDisj [[p, q]]  = [Node p [Node q []]]
fromDisj [[p]]     = [Node p []]
fromDisj []        = []



-- auxiliary function to expand a formula
expandFormula :: Formula  -> Proof [[Formula]]

-- conjuction and disjunction
expandFormula (And p q) = return [[p,q]]
expandFormula (Or p q)  = return [[p],[q]]

-- implication
expandFormula (Implies p q) = return [[Not p],[q]]

-- quantification
expandFormula (Forall x p) 
    = do x'<-newVar
         let s = Map.singleton x (Var x')
         return [[subst s p]]
        
expandFormula f@(Exist x p) 
    = do t<-newSkolem (fv f)
         let s = Map.singleton x t
         return [[subst s p]]

-- negated forms
expandFormula (Not TT) = return [[FF]]
expandFormula (Not FF) = return [[TT]]

expandFormula (Not (Not p)) = return [[p]]

expandFormula (Not (And p q)) 
    = return [[Not p], [Not q]]

expandFormula (Not (Or p q)) 
    = return [[Not p, Not q]]

expandFormula (Not (Implies p q)) 
    = return [[p, Not q]]

expandFormula (Not (Forall x p)) 
    = return [[Exist x (Not p)]]

expandFormula (Not (Exist x p)) 
    = return [[Forall x (Not p)]]

-- default rule: no expansion 
expandFormula f = return [[f]]



-- use resolution to attempt to close the current branch
resolve :: Tableau -> Tableau
resolve loc 
    = case msum [resolve_atom f f' | 
                 f'<-map formula (ancestorLabels loc)] of
        Nothing -> loc
        Just s -> update_closed $ 
                  modifyTree (incr_uses . close) (subst s loc)
    where f = formula (rootLabel (tree loc))
          close (Node x _) = Node (x{is_open=False}) [Node (attr FF) []]


-- resolution of two atomic formulas
resolve_atom :: Formula -> Formula -> Maybe Subst
resolve_atom (Rel r ts) (Not (Rel r' ts'))
    | r==r' && length ts==length ts' = unifyEqs Map.empty (zip ts ts')
resolve_atom f@(Not (Rel r ts)) f'@(Rel r' ts') = resolve_atom f' f
resolve_atom _ _ = Nothing



-- check whether a formula is a positive/negative literal
atomic :: Formula -> Bool
atomic (Rel r ts)       = True
atomic (Not (Rel r ts)) = True
atomic _                = False


-- list the ancestors of a tree location
ancestorLabels :: TreeLoc a -> [a]
ancestorLabels = map (rootLabel.tree) . ancestors 

ancestors :: TreeLoc a -> [TreeLoc a]
ancestors loc = loc : maybe [] ancestors (parent loc)



-- move the cursor (leaving the position unchanged when not applicable)
cursorLeft, cursorRight, cursorUp, cursorDown :: TreeLoc a -> TreeLoc a
cursorLeft loc  = maybe loc id (left loc)
cursorRight loc = maybe loc id (right loc)
cursorUp loc    = maybe loc id (parent loc)
cursorDown loc  = maybe loc id (firstChild loc)


-- collect all leaves of a tree
leaves :: Tree a -> [a]
leaves (Node x []) = [x]
leaves (Node _ ts) = concatMap leaves ts



-- update open/closed attributes
update_closed :: Tableau -> Tableau
update_closed loc
    | is_open_branch loc = loc
    | otherwise 
        = let loc' = close_node loc
          in maybe loc' update_closed (parent loc')

close_node :: Tableau -> Tableau
close_node = modifyTree (\(Node f ts) -> Node (f{is_open=False}) ts) 


-- check if the current node is an open branch
is_open_branch ::  Tableau -> Bool
is_open_branch loc = or (map (is_open . rootLabel) (subForest (tree loc)))