{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
module Zeno.Clause (
  Equality (..), Clause (..), 
  Quantified (..), Hypothesis (..),
  flipEquality, flipQuantifiedClauseEquality,
  equalityToPair, pairToEquality, 
  addCondition, removeCondition,
) where

import Prelude ()
import Zeno.Prelude
import Zeno.Expression
import Zeno.Traversing

data Equality a 
  = (:=:)       { equalityLeft :: !(Expr a),
                  equalityRight :: !(Expr a) }
  deriving ( Eq, Functor, Foldable, Traversable )

data Clause a
  = Clause      { clauseEquality :: !(Equality a),
                  clauseConditions :: ![Equality a] }
  deriving ( Eq, Functor, Foldable, Traversable )
  
data Quantified f a
  = Quantified  { quantifiedVariables :: ![a],
                  quantifiedObject :: !(f a) }
  deriving ( Eq, Functor, Foldable, Traversable )
  
data Hypothesis a 
  = Hypothesis  { hypId :: !a,
                  hypBinds :: ![Binding a], 
                  hypClause :: !(Quantified Clause a) }
  deriving ( Functor, Foldable, Traversable )
  
instance Eq a => Eq (Hypothesis a) where
  (==) = (==) `on` hypId
  
instance Ord a => Ord (Hypothesis a) where
  compare = compare `on` hypId
  
instance ExprTraversable Equality where
  mapExprM f (lhs :=: rhs) =
    return (:=:) `ap` f lhs `ap` f rhs
    
instance ExprTraversable Clause where
  mapExprM f (Clause eq conds) = 
    return Clause `ap` mapExprM f eq `ap` mapM (mapExprM f) conds
    
instance ExprTraversable (Quantified Clause) where
  mapExprM f (Quantified vars cls) =
    return (Quantified vars) `ap` mapExprM f cls
    
instance ExprTraversable Hypothesis where
  mapExprM f (Hypothesis id binds cls) = 
    return (Hypothesis id) `ap` mapM mapBind binds `ap` mapExprM f cls
    where mapBind (b, expr) = do
            expr' <- f expr 
            return (b, expr')
            
instance WithinTraversable (Expr a) (Equality a) where
  mapWithinM f (t1 :=: t2) = do
    t1' <- mapWithinM f t1
    t2' <- mapWithinM f t2
    return (t1' :=: t2')
  
instance WithinTraversable (Expr a) (Clause a) where
  mapWithinM f (Clause eq conds) = do
    eq' <- mapWithinM f eq
    conds' <- mapM (mapWithinM f) conds
    return (Clause eq' conds')
    
instance WithinTraversable c (a b) => 
         WithinTraversable c (Quantified a b) where
  mapWithinM f (Quantified vars obj) = do
    obj' <- mapWithinM f obj
    return (Quantified vars obj')
    
instance WithinTraversable (Expr a) (Hypothesis a) where
  mapWithinM f (Hypothesis id binds cls) =
    Hypothesis id binds `liftM` mapWithinM f cls
    
instance (Show b, Show (a b)) => Show (Quantified a b) where
  show (Quantified vars obj) = 
    case vars of
      [] -> show obj
      _ -> "forall " ++ (intercalate ", " $ map show vars) 
        ++ " . " ++ show obj
  
instance Show a => Show (Hypothesis a) where
  show = show . hypClause
        
instance Show a => Show (Equality a) where
  show (l :=: r) = show l ++ " = " ++ show r

instance Show a => Show (Clause a) where
  show (Clause t cs) = 
    let cs_s = case cs of
          [] -> ""
          cs -> " :- " 
            ++ intercalate ", " (map show cs)
    in show t ++ cs_s
    
flipEquality :: Equality a -> Equality a 
flipEquality (l :=: r) = r :=: l

equalityToPair :: Equality a -> (Expr a, Expr a)
equalityToPair (l :=: r) = (l, r)

pairToEquality :: (Expr a, Expr a) -> Equality a
pairToEquality = uncurry (:=:)

flipClauseEquality :: Clause a -> Clause a
flipClauseEquality cs = cs 
  { clauseEquality = flipEquality (clauseEquality cs) }
  
flipQuantifiedClauseEquality :: Quantified Clause a -> Quantified Clause a
flipQuantifiedClauseEquality q = q
  { quantifiedObject = flipClauseEquality (quantifiedObject q) }

addCondition :: Equality a -> Clause a -> Clause a
addCondition eq cs = cs 
  { clauseConditions = clauseConditions cs ++ [eq] }
  
removeCondition :: Eq a => Equality a -> Clause a -> Clause a
removeCondition cond (Clause eq conds) =
  Clause eq (delete cond conds)