{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, FunctionalDependencies,
             GeneralizedNewtypeDeriving, MultiParamTypeClasses, TemplateHaskell, UndecidableInstances #-}
{-# OPTIONS -fno-warn-missing-signatures -fno-warn-orphans #-}
-- |Data types which are instances of the Logic type class for use
-- when you just want to use the classes and you don't have a
-- particular representation you need to use.
module Data.Logic.Types.FirstOrder
    ( Formula(..)
    , PTerm(..)
    ) where

import Data.Data (Data)
import Data.Logic.Classes.Arity (Arity)
import Data.Logic.Classes.Boolean (Boolean(..))
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), showFirstOrder, Quant(..), Predicate(..))
import Data.Logic.Classes.Literal (Literal(..), PredicateLit(..))
import Data.Logic.Classes.Logic (Logic(..))
import Data.Logic.Classes.Negatable(Negatable(..))
import Data.Logic.Classes.Pred (Pred(..), pApp)
import Data.Logic.Classes.Propositional (Combine(..), BinOp(..))
import Data.Logic.Classes.Skolem (Skolem(..))
import Data.Logic.Classes.Term (Term(..), showTerm)
import Data.Logic.Classes.Variable (Variable)
import Data.Logic.Classes.Propositional (PropositionalFormula(..))
import Data.SafeCopy (base, deriveSafeCopy)
import Data.Typeable (Typeable)
import Happstack.Data (deriveNewData)

-- | The range of a formula is {True, False} when it has no free variables.
data Formula v p f
    = Predicate (Predicate p (PTerm v f))
    | Combine (Combine (Formula v p f))
    | Quant Quant v (Formula v p f)
    -- Note that a derived Eq instance is not going to tell us that
    -- a&b is equal to b&a, let alone that ~(a&b) equals (~a)|(~b).
    deriving (Eq,Ord,Read,Data,Typeable)

-- | The range of a term is an element of a set.
data PTerm v f
    = Var v                         -- ^ A variable, either free or
                                    -- bound by an enclosing quantifier.
    | FunApp f [PTerm v f]           -- ^ Function application.
                                    -- Constants are encoded as
                                    -- nullary functions.  The result
                                    -- is another term.
    deriving (Eq,Ord,Read,Data,Typeable)

-- data InfixPred = (:=:) | (:!=:) deriving (Eq,Ord,Show,Data,Typeable,Enum,Bounded)

-- |We need to implement read manually here due to
-- <http://hackage.haskell.org/trac/ghc/ticket/4136>
{-
instance Read InfixPred where
    readsPrec _ s =
        map (\ (x, t) -> (x, drop (length t) s))
            (take 1 (dropWhile (\ (_, t) -> not (isPrefixOf t s)) prs))
        where
          prs = [((:=:), ":=:"),
                 ((:!=:), ":!=:")]
-}

instance (FirstOrderFormula (Formula v p f) (PTerm v f) v p f, Show v, Show p, Show f) => Show (Formula v p f) where
    show = showFirstOrder

instance (FirstOrderFormula (Formula v p f) (PTerm v f) v p f, Show v, Show p, Show f) => Show (PTerm v f) where
    show = showTerm

instance Negatable (Formula v p f) where
    (.~.) (Combine ((:~:) (Combine ((:~:) x)))) = (.~.) x
    (.~.) (Combine ((:~:) x)) = x
    (.~.) x = Combine ((:~:) x)
    negated (Combine ((:~:) x)) = not (negated x)
    negated _ = False

instance (Ord v, Ord p, Ord f) => Logic (Formula v p f) where
    x .<=>. y = Combine (BinOp  x (:<=>:) y)
    x .=>.  y = Combine (BinOp  x (:=>:)  y)
    x .|.   y = Combine (BinOp  x (:|:)   y)
    x .&.   y = Combine (BinOp  x (:&:)   y)

instance (Ord v, Variable v, Data v,
          Ord p, Boolean p, Arity p, Data p,
          Ord f, Skolem f, Data f,
          Boolean (Formula v p f), Logic (Formula v p f)) =>
         PropositionalFormula (Formula v p f) (Formula v p f) where
    atomic (Predicate (Equal t1 t2)) = t1 .=. t2
    atomic (Predicate (NotEqual t1 t2)) = t1 .!=. t2
    atomic (Predicate (Apply p ts)) = pApp p ts
    atomic _ = error "atomic method of PropositionalFormula for Parameterized: invalid argument"
    foldPropositional c a formula =
        case formula of
          Quant _ _ _ -> error "foldF0: quantifiers should not be present"
          Combine x -> c x
          Predicate x -> a (Predicate x)

instance (Ord v, Variable v, Data v, Eq f, Ord f, Skolem f, Data f) => Term (PTerm v f) v f where
    foldTerm vf fn t =
        case t of
          Var v -> vf v
          FunApp f ts -> fn f ts
    zipT v f t1 t2 =
        case (t1, t2) of
          (Var v1, Var v2) -> v v1 v2
          (FunApp f1 ts1, FunApp f2 ts2) -> f f1 ts1 f2 ts2
          _ -> Nothing
    var = Var
    fApp x args = FunApp x args

instance (Ord v, Ord p, Boolean p, Arity p, Ord f) => Pred p (PTerm v f) (Formula v p f) where
    pApp0 x = Predicate (Apply x [])
    pApp1 x a = Predicate (Apply x [a])
    pApp2 x a b = Predicate (Apply x [a,b])
    pApp3 x a b c = Predicate (Apply x [a,b,c])
    pApp4 x a b c d = Predicate (Apply x [a,b,c,d])
    pApp5 x a b c d e = Predicate (Apply x [a,b,c,d,e])
    pApp6 x a b c d e f = Predicate (Apply x [a,b,c,d,e,f])
    pApp7 x a b c d e f g = Predicate (Apply x [a,b,c,d,e,f,g])
    x .=. y = Predicate (Equal x y)
    x .!=. y = Predicate (NotEqual x y)

instance (Pred p (PTerm v f) (Formula v p f),
          Variable v, Ord v, Data v, Show v,
          Ord p, Data p, Show p,
          Skolem f, Ord f, Data f, Show f) =>
         FirstOrderFormula (Formula v p f) (PTerm v f) v p f where
    for_all v x = Quant All v x
    exists v x = Quant Exists v x
    foldFirstOrder q c p f =
        case f of
          Quant op v f' -> q op v f'
          Combine x -> c x
          Predicate x -> p x
    zipFirstOrder q c p f1 f2 =
        case (f1, f2) of
          (Quant q1 v1 f1', Quant q2 v2 f2') -> q q1 v1 (Quant q1 v1 f1') q2 v2 (Quant q2 v2 f2')
          (Combine x, Combine y) -> c x y
          (Predicate x, Predicate y) -> p x y
          _ -> Nothing

instance (Variable v, Ord v, Data v, Show v,
          Arity p, Boolean p, Ord p, Data p, Show p,
          Skolem f, Ord f, Data f, Show f) => Literal (Formula v p f) (PTerm v f) v p f where
    equals x y = Predicate (Equal x y)
    pAppLiteral p ts = Predicate (Apply p ts)
    foldLiteral c pr l =
        case l of
          (Combine ((:~:) x)) -> c x
          (Predicate (Apply p ts)) -> pr (ApplyLit p ts)
          (Predicate (Equal x y)) -> pr (EqualLit x y)
          _ -> error "Invalid formula used as Literal instance"
    zipLiterals c pr l1 l2 =
        case (l1, l2) of
          (Combine ((:~:) x), Combine ((:~:) y)) -> c x y
          (Predicate (Apply p1 ts1), Predicate (Apply p2 ts2)) -> pr (ApplyLit p1 ts1) (ApplyLit p2 ts2)
          _ -> Nothing

$(deriveSafeCopy 1 'base ''PTerm)
$(deriveSafeCopy 1 'base ''Formula)

$(deriveNewData [''PTerm, ''Formula])