{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ViewPatterns #-}
-- |
-- Copyright   : (c) 2010-2012 Benedikt Schmidt & Simon Meier
-- License     : GPL v3 (see LICENSE)
--
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- Terms with variables and constants.

module Term.VTerm (
    -- * Terms with constants and variables
      Lit(..)
    , VTerm

    , varTerm
    , constTerm
    , varsVTerm
    , occursVTerm
    , constsVTerm
    , isVar

    -- ** Destructors
    , termVar
    , termVar'

    , IsVar
    , IsConst
    , module Term.Term
    ) where

import Data.Foldable
import Data.Traversable
import qualified Data.DList as D
import Data.Typeable
import Data.Generics
import Data.DeriveTH
import Data.Binary
import Data.Monoid
import Control.DeepSeq
import Control.Basics

import Extension.Prelude

import Safe (fromJustNote)

import Term.Term

----------------------------------------------------------------------
-- Terms with constants and variables
----------------------------------------------------------------------

-- | A Lit is either a constant or a variable. (@Const@ is taken by Control.Applicative)
data Lit c v = Con c | Var v
  deriving (Eq, Ord, Data, Typeable)

-- | A VTerm is a term with constants and variables
type VTerm c v = Term (Lit c v)

-- | collect class constraints for variables
class (Ord v, Eq v, Show v) => IsVar v where

-- | collect class constraints for constants
class (Ord c, Eq c, Show c, Data c) => IsConst c where

-- | Functor instance in the variable.
instance Functor (Lit c) where
    fmap f (Var v)  = Var (f v)
    fmap _ (Con c) = Con c

-- | Foldable instance in the variable.
instance Foldable (Lit c) where
    foldMap f (Var v)  = f v
    foldMap _ (Con _) = mempty

-- | Traversable instance in the variable.
instance Traversable (Lit c) where
    sequenceA (Var v)  = Var <$> v
    sequenceA (Con n) = pure $ Con n

-- | Applicative instance in the variable.
instance Applicative (Lit c) where
    pure = Var
    (Var f)  <*> (Var x)  = Var (f x)
    (Var _)  <*> (Con n) = Con n
    (Con n) <*> _        = Con n

-- | Monad instance in the variable
instance Monad (Lit c) where
    return         = Var
    (Var x)  >>= f = f x
    (Con n)  >>= _ = Con n

instance Sized (Lit c v) where
    size _ = 1

instance (Show v, Show c) => Show (Lit c v) where
    show (Var x) = show x
    show (Con n) = show n

-- | @varTerm v@ is the 'VTerm' with the variable @v@.
varTerm :: v -> VTerm c v
varTerm = lit . Var

-- | @constTerm c@ is the 'VTerm' with the const @c@.
constTerm :: c -> VTerm c v
constTerm = lit . Con

-- | @isVar t returns @True@ if @t@ is a variable.
isVar :: VTerm c v -> Bool
isVar (viewTerm -> Lit (Var _)) = True
isVar _ = False

-- | @vars t@ returns a duplicate-free list of variables that occur in @t@.
varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]
varsVTerm = sortednub . D.toList . foldMap (foldMap return)

-- | @occurs v t@ returns @True@ if @v@ occurs in @t@
occursVTerm :: Eq v => v -> VTerm c v -> Bool
occursVTerm v = getAny . foldMap (foldMap (Any . (v==)))

-- | @constsVTerm t@ returns a duplicate-free list of constants that occur in @t@.
constsVTerm :: IsConst c => VTerm c v -> [c]
constsVTerm = sortednub . D.toList . foldMap fLit
  where fLit (Var _)  = mempty
        fLit (Con n) = return n

-- Destructors
--------------

-- | Extract just the variable from a term that may be variable.
termVar :: VTerm c v -> Maybe v
termVar (viewTerm -> Lit (Var v)) = Just v
termVar _                         = Nothing

-- | Extract just the variable from a term that must be variable, throw an
-- error if this fails.
termVar' :: (Show c, Show v) => VTerm c v -> v
termVar' t =
    fromJustNote ("termVar': non-variable term " ++ show t) (termVar t)


-- Derived instances
--------------------

$( derive makeNFData ''Lit)
$( derive makeBinary ''Lit)