{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeSynonymInstances       #-}
{-# LANGUAGE ViewPatterns               #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
  -- spurious warnings for view patterns
-- |
-- Copyright   : (c) 2010-2012 Benedikt Schmidt & Simon Meier
-- License     : GPL v3 (see LICENSE)
--
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- Terms with logical variables  and names.
module Term.LTerm (

  -- * Names
    Name(..)
  , NameTag(..)
  , NameId(..)

  , NTerm

  -- ** Queries
  , sortOfName

  -- ** Construction
  , freshTerm
  , pubTerm

  -- * LVar
  , LSort(..)
  , LVar(..)
  , NodeId
  , LTerm
  , LNTerm

  , freshLVar
  , sortPrefix
  , sortSuffix
  , sortCompare
  , sortOfLTerm
  , sortOfLNTerm
  , sortOfLit
  , isMsgVar
  , isFreshVar
  , isSimpleTerm
  , niFactors
  , containsPrivate
  , neverContainsFreshPriv

  -- ** Destructors
  , ltermVar
  , ltermVar'
  , ltermNodeId
  , ltermNodeId'
  , bltermNodeId
  , bltermNodeId'


  -- ** Manging Free LVars

  , HasFrees(..)
  , MonotoneFunction(..)
  , occurs
  , freesList
  , frees
  , someInst
  , rename
  , eqModuloFreshnessNoAC
  , avoid
  , evalFreshAvoiding
  , evalFreshTAvoiding
  , renameAvoiding
  , avoidPrecise
  , renamePrecise
  , renameDropNamehint
  , varOccurences

  -- * BVar
  , BVar(..)
  , BLVar
  , BLTerm
  , foldBVar
  , fromFree

  -- * Pretty-Printing
  , prettyLVar
  , prettyNodeId
  , prettyNTerm
  , prettyLNTerm

  -- * Convenience exports
  , module Term.VTerm
) where

import           Term.Rewriting.Definitions
import           Term.VTerm

import           Text.PrettyPrint.Class

import           Control.Applicative
import           Control.DeepSeq
import           Control.Monad.Bind
import           Control.Monad.Identity
import qualified Control.Monad.Trans.PreciseFresh as Precise

import           Data.Binary
import qualified Data.DList                       as D
import           Data.DeriveTH
import           Data.Foldable                    hiding (concatMap, elem, notElem, any)
import           Data.Generics                    hiding (GT)
import qualified Data.Map                         as M
import           Data.Monoid
import qualified Data.Set                         as S
import           Data.Traversable
import qualified Data.ByteString.Char8            as BC

import           Safe                             (fromJustNote)

import           Extension.Data.Monoid
import           Extension.Prelude

import           Logic.Connectives

------------------------------------------------------------------------------
-- Sorts.
------------------------------------------------------------------------------

-- | Sorts for logical variables. They satisfy the following sub-sort relation:
--
-- >  LSortFresh < LSortMsg
-- >  LSortPub   < LSortMsg
--
data LSort = LSortPub   -- ^ Arbitrary public names.
           | LSortFresh -- ^ Arbitrary fresh names.
           | LSortMsg   -- ^ Arbitrary messages.
           | LSortNode  -- ^ Sort for variables denoting nodes of derivation graphs.
           deriving( Eq, Ord, Show, Enum, Bounded, Typeable, Data )

-- | @sortCompare s1 s2@ compares @s1@ and @s2@ with respect to the partial order on sorts.
--   Partial order: Node      Msg
--                           /   \
--                         Pub  Fresh
sortCompare :: LSort -> LSort -> Maybe Ordering
sortCompare s1 s2 = case (s1, s2) of
    (a, b) | a == b          -> Just EQ
    -- Node is incomparable to all other sorts, invalid input
    (LSortNode,  _        )  -> Nothing
    (_,          LSortNode)  -> Nothing
    -- Msg is greater than all sorts except Node
    (LSortMsg,   _        )  -> Just GT
    (_,          LSortMsg )  -> Just LT
    -- The remaining combinations (Pub/Fresh) are incomparable
    _                        -> Nothing

-- | @sortPrefix s@ is the prefix we use for annotating variables of sort @s@.
sortPrefix :: LSort -> String
sortPrefix LSortMsg   = ""
sortPrefix LSortFresh = "~"
sortPrefix LSortPub   = "$"
sortPrefix LSortNode  = "#"

-- | @sortSuffix s@ is the suffix we use for annotating variables of sort @s@.
sortSuffix :: LSort -> String
sortSuffix LSortMsg   = "msg"
sortSuffix LSortFresh = "fresh"
sortSuffix LSortPub   = "pub"
sortSuffix LSortNode  = "node"


------------------------------------------------------------------------------
-- Names
------------------------------------------------------------------------------

-- | Type safety for names.
newtype NameId = NameId { getNameId :: String }
    deriving( Eq, Ord, Typeable, Data, NFData, Binary )

-- | Tags for names.
data NameTag = FreshName | PubName
    deriving( Eq, Ord, Show, Typeable, Data )

-- | Names.
data Name = Name {nTag :: NameTag, nId :: NameId}
    deriving( Eq, Ord, Typeable, Data )

-- | Terms with literals containing names and arbitrary variables.
type NTerm v = VTerm Name v


-- Instances
------------

instance IsConst Name where

instance Show Name where
  show (Name FreshName n) = "~'" ++ show n ++ "'"
  show (Name PubName   n) = "'"  ++ show n ++ "'"

instance Show NameId where
  show = getNameId

-- Construction of terms with names
-----------------------------------

-- | @freshTerm f@ represents the fresh name @f@.
freshTerm :: String -> NTerm v
freshTerm = lit . Con . Name FreshName . NameId

-- | @pubTerm f@ represents the pub name @f@.
pubTerm :: String -> NTerm v
pubTerm = lit . Con . Name PubName . NameId

-- | Return 'LSort' for given 'Name'.
sortOfName :: Name -> LSort
sortOfName (Name FreshName _) = LSortFresh
sortOfName (Name PubName   _) = LSortPub

------------------------------------------------------------------------------
-- LVar: logical variables
------------------------------------------------------------------------------


-- | Logical variables. Variables with the same name and index but different
-- sorts are regarded as different variables.
data LVar = LVar
     { lvarName :: String
     , lvarSort :: !LSort     -- FIXME: Rename to 'sortOfLVar' for consistency
                              -- with the other 'sortOf' functions.
     , lvarIdx  :: !Integer
     }
     deriving( Typeable, Data )

-- | An alternative name for logical variables, which are intented to be
-- variables of sort 'LSortNode'.
type NodeId = LVar

-- | Terms used for proving; i.e., variables fixed to logical variables.
type LTerm c = VTerm c LVar

-- | Terms used for proving; i.e., variables fixed to logical variables
--   and constants to Names.
type LNTerm = VTerm Name LVar

-- | @freshLVar v@ represents a fresh logical variable with name @v@.
freshLVar :: MonadFresh m => String -> LSort -> m LVar
freshLVar n s = LVar n s <$> freshIdent n

-- | Returns the most precise sort of an 'LTerm'.
sortOfLTerm :: Show c => (c -> LSort) -> LTerm c -> LSort
sortOfLTerm sortOfConst t = case viewTerm2 t of
    Lit2 (Con c)  -> sortOfConst c
    Lit2 (Var lv) -> lvarSort lv
    _             -> LSortMsg

-- | Returns the most precise sort of an 'LNTerm'.
sortOfLNTerm :: LNTerm -> LSort
sortOfLNTerm = sortOfLTerm sortOfName

-- | Returns the most precise sort of a 'Lit'.
sortOfLit :: Lit Name LVar -> LSort
sortOfLit (Con n) = sortOfName n
sortOfLit (Var v) = lvarSort v


-- | Is a term a message variable?
isMsgVar :: LNTerm -> Bool
isMsgVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortMsg)
isMsgVar _                         = False

-- | Is a term a fresh variable?
isFreshVar :: LNTerm -> Bool
isFreshVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortFresh)
isFreshVar _                         = False

-- | The non-inverse factors of a term.
niFactors :: LNTerm -> [LNTerm]
niFactors t = case viewTerm2 t of
                FMult ts -> concatMap niFactors ts
                FInv t1  -> niFactors t1
                _        -> [t]

-- | @containsPrivate t@ returns @True@ if @t@ contains private function symbols.
containsPrivate :: Term t -> Bool
containsPrivate t = case viewTerm t of
    Lit _                          -> False
    FApp (NoEq (_,(_,Private))) _  -> True
    FApp _                      as -> any containsPrivate as

-- | A term is *simple* iff there is an instance of this term that can be
-- constructed from public names only. i.e., the term does not contain any
-- fresh names, fresh variables, or private function symbols.
isSimpleTerm :: LNTerm -> Bool
isSimpleTerm t =
    not (containsPrivate t) && 
    (getAll . foldMap (All . (LSortFresh /=) . sortOfLit) $ t)

-- | 'True' iff no instance of this term contains fresh names or private function symbols.
neverContainsFreshPriv :: LNTerm -> Bool
neverContainsFreshPriv t =
    not (containsPrivate t) && 
    (getAll . foldMap (All . (`notElem` [LSortMsg, LSortFresh]) . sortOfLit) $ t)

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

-- | Extract a variable of the given sort from a term that may be such a
-- variable. Use 'termVar', if you do not want to restrict the sort.
ltermVar :: LSort -> LTerm c -> Maybe LVar
ltermVar s t = do v <- termVar t; guard (s == lvarSort v); return v

-- | Extract a variable of the given sort from a term that must be such a
-- variable. Fails with an error, if that is not possible.
ltermVar' :: Show c => LSort -> LTerm c -> LVar
ltermVar' s t =
    fromJustNote err (ltermVar s t)
  where
    err = "ltermVar': expected variable term of sort " ++ show s ++ ", but got " ++ show t

-- | Extract a node-id variable from a term that may be a node-id variable.
ltermNodeId  :: LTerm c -> Maybe LVar
ltermNodeId = ltermVar LSortNode

-- | Extract a node-id variable from a term that must be a node-id variable.
ltermNodeId' :: Show c => LTerm c -> LVar
ltermNodeId' = ltermVar' LSortNode


-- BVar: Bound variables
------------------------

-- | Bound and free variables.
data BVar v = Bound Integer  -- ^ A bound variable in De-Brujin notation.
            | Free  v        -- ^ A free variable.
            deriving( Eq, Ord, Show, Data, Typeable )

-- | 'LVar's combined with quantified variables. They occur only in 'LFormula's.
type BLVar = BVar LVar

-- | Terms built over names and 'LVar's combined with quantified variables.
type BLTerm = NTerm BLVar


-- | Fold a possibly bound variable.
{-# INLINE foldBVar #-}
foldBVar :: (Integer -> a) -> (v -> a) -> BVar v -> a
foldBVar fBound fFree = go
  where
    go (Bound i) = fBound i
    go (Free v)  = fFree v

instance Functor BVar where
    fmap f = foldBVar Bound (Free . f)

instance Foldable BVar where
    foldMap f = foldBVar mempty f

instance Traversable BVar where
    traverse f = foldBVar (pure . Bound) (fmap Free . f)

instance Applicative BVar where
   pure  = return
   (<*>) = ap

instance Monad BVar where
    return  = Free
    m >>= f = foldBVar Bound f m

-- | Extract the name of free variable under the assumption the variable is
-- guaranteed to be of the form @Free a@.
fromFree :: BVar v -> v
fromFree (Free v)  = v
fromFree (Bound i) = error $ "fromFree: bound variable '" ++ show i ++ "'"

-- | Extract a node-id variable from a term that may be a node-id variable.
bltermNodeId  :: BLTerm -> Maybe LVar
bltermNodeId t = do
    Free v <- termVar t; guard (LSortNode == lvarSort v); return v

-- | Extract a node-id variable from a term that must be a node-id variable.
bltermNodeId' :: BLTerm -> LVar
bltermNodeId' t =
    fromJustNote err (bltermNodeId t)
  where
    err = "bltermNodeId': expected free node-id variable term, but got " ++
           show t

-- Instances
------------

instance Eq LVar where
  (LVar n1 s1 i1) == (LVar n2 s2 i2) = i1 == i2 && s1 == s2 && n1 == n2

-- An ord instance that prefers the 'lvarIdx' over the 'lvarName'.
instance Ord LVar where
    compare (LVar x1 x2 x3) (LVar y1 y2 y3) =
        compare x3 y3 & compare x2 y2 & compare x1 y1 & EQ
      where
        EQ & x = x
        x  & _ = x

instance Show LVar where
    show (LVar v s i) =
        sortPrefix s ++ body
      where
        body | null v           = show i
--             | isDigit (last v) = v ++ "." ++ show i
             | i == 0           = v
             | otherwise        = v ++ "." ++ show i

instance IsVar LVar where

------------------------------------------------------------------------------
-- Managing bound and free LVars
------------------------------------------------------------------------------


-- | This type captures the occurence of a variable in a certain context.
type Occurence = [String]

-- | For performance reasons, we distinguish between monotone functions on
-- 'LVar's and arbitrary functions. For a monotone f, if @x <= y@, then
-- @f x <= f y@. This ensures that the AC-normal form does not have
-- to be recomputed. If you are unsure about what to use, then use the
-- 'Arbitrary' function.
data MonotoneFunction f = Monotone (LVar -> f LVar )
                        | Arbitrary (LVar -> f LVar )

-- | @HasFree t@ denotes that the type @t@ has free @LVar@ variables. They can
-- be collected using 'foldFrees' and 'foldFreesOcc' and mapped in the context
-- of an applicative functor using 'mapFrees'.
--
-- When defining instances of this class, you have to ensure that only the free
-- LVars are collected and mapped and no others. The instances for standard
-- Haskell types assume that all variables free in all type arguments are free.
-- The 'foldFreesOcc' is only used to define the function 'varOccurences'. See
-- below for required properties of the instance methods.
--
-- Once we need it, we can use type synonym instances to parametrize over the
-- variable type.
--
class HasFrees t where
    foldFrees  :: Monoid m      => (LVar -> m      ) -> t -> m
    foldFreesOcc :: Monoid m => (Occurence -> LVar -> m) -> Occurence -> t -> m
    mapFrees   :: Applicative f => MonotoneFunction f -> t -> f t

-- | @v `occurs` t@ iff variable @v@ occurs as a free variable in @t@.
occurs :: HasFrees t => LVar -> t -> Bool
occurs x = getAny . foldFrees (Any . (x ==))

-- | @freesDList t@ is the difference list of all free variables of @t@.
freesDList :: HasFrees t => t -> D.DList LVar
freesDList = foldFrees pure

-- | @freesList t@ is the list of all free variables of @t@.
freesList :: HasFrees t => t -> [LVar]
freesList = D.toList . freesDList

-- | @frees t@ is the sorted and duplicate-free list of all free variables in
-- @t@.
frees :: HasFrees t => t -> [LVar]
frees = sortednub . freesList

-- | Returns the variables occuring in @t@ together with the contexts they appear in.
-- Note that certain contexts (and variables only occuring in such contexts) are
-- ignored by this function.
-- The function is used to "guess" renamings of variables, i.e., if t is a renaming of s,
-- then variables that occur in equal contexts in t and s are probably renamings of
-- each other.
varOccurences :: HasFrees a => a -> [(LVar, S.Set Occurence)]
varOccurences t =
    map (\((v,ctx1):rest) -> (v, S.fromList (ctx1:(map snd rest)))) . groupOn fst . sortOn fst
    . foldFreesOcc (\ c v -> [(v,c)]) [] $ t

-- | @someInst t@ returns an instance of @t@ where all free variables whose
-- binding is not yet determined by the caller are replaced with fresh
-- variables.
someInst :: (MonadFresh m, MonadBind LVar LVar m, HasFrees t) => t -> m t
someInst = mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x (lvarName x))

-- | @rename t@ replaces all variables in @t@ with fresh variables.
--   Note that the result is not guaranteed to be equal for terms that are
--   equal modulo changing the indices of variables.
rename :: (MonadFresh m, HasFrees a) => a -> m a
rename x = case boundsVarIdx x of
    Nothing                     -> return x
    Just (minVarIdx, maxVarIdx) -> do
      freshStart <- freshIdents (succ (maxVarIdx - minVarIdx))
      return . runIdentity . mapFrees (Monotone $ incVar (freshStart - minVarIdx)) $ x
  where
    incVar shift (LVar n so i) = pure $ LVar n so (i+shift)

-- | @eqModuloFreshness t1 t2@ checks whether @t1@ is equal to @t2@ modulo
-- renaming of indices of free variables. Note that the normal form is not
-- unique with respect to AC symbols.
eqModuloFreshnessNoAC :: (HasFrees a, Eq a) => a -> a -> Bool
eqModuloFreshnessNoAC t1 =
     -- this formulation shares normalisation of t1 among further calls to
     -- different t2.
    (normIndices t1 ==) . normIndices
  where
    normIndices = (`evalFresh` nothingUsed) . (`evalBindT` noBindings) .
                  mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x "")

-- | The mininum and maximum index of all free variables.
boundsVarIdx :: HasFrees t => t -> Maybe (Integer, Integer)
boundsVarIdx = getMinMax . foldFrees (minMaxSingleton . lvarIdx)

-- | @avoid t@ computes a 'FreshState' that avoids generating
-- variables occurring in @t@.
avoid :: HasFrees t => t -> FreshState
avoid = maybe 0 (succ . snd) . boundsVarIdx

-- | @m `evalFreshAvoiding` t@ evaluates the monadic action @m@ with a
-- fresh-variable supply that avoids generating variables occurring in @t@.
evalFreshAvoiding :: HasFrees t => Fresh a -> t -> a
evalFreshAvoiding m = evalFresh m . avoid

-- | @m `evalFreshTAvoiding` t@ evaluates the monadic action @m@ in the
-- underlying monad with a fresh-variable supply that avoids generating
-- variables occurring in @t@.
evalFreshTAvoiding :: (Monad m, HasFrees t) => FreshT m a -> t -> m a
evalFreshTAvoiding m = evalFreshT m . avoid

-- | @s `renameAvoiding` t@ replaces all free variables in @s@ by
--   fresh variables avoiding variables in @t@.
renameAvoiding :: (HasFrees s, HasFrees t) => s -> t -> s
s `renameAvoiding` t = rename s `evalFreshAvoiding` t

-- | @avoidPrecise t@ computes a 'Precise.FreshState' that avoids generating
-- variables occurring in @t@.
avoidPrecise :: HasFrees t => t -> Precise.FreshState
avoidPrecise =
    foldl' ins M.empty . frees
  where
    ins m v = M.insertWith' max (lvarName v) (lvarIdx v + 1) m

-- | @renamePrecise t@ replaces all variables in @t@ with fresh variables.
--   If 'Control.Monad.PreciseFresh' is used with non-AC terms and identical
--   fresh state, the same result is returned for two terms that only differ
--   in the indices of variables.
renamePrecise :: (MonadFresh m, HasFrees a) => a -> m a
renamePrecise x = evalBindT (someInst x) noBindings


renameDropNamehint :: (MonadFresh m, MonadBind LVar LVar m, HasFrees a) => a -> m a
renameDropNamehint =
    mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x "")


-- Instances
------------

instance HasFrees LVar where
    foldFrees = id
    foldFreesOcc f c v = f c v
    mapFrees (Arbitrary f) = f
    mapFrees (Monotone f)  = f

instance HasFrees v => HasFrees (Lit c v) where
    foldFrees f (Var x) = foldFrees f x
    foldFrees _ _       = mempty

    foldFreesOcc f c (Var x) = foldFreesOcc f c x
    foldFreesOcc _ _ _       = mempty

    mapFrees f (Var x) = Var <$> mapFrees f x
    mapFrees _ l       = pure l

instance HasFrees v => HasFrees (BVar v) where
    foldFrees _ (Bound _) = mempty
    foldFrees f (Free v)  = foldFrees f v

    foldFreesOcc _ _ (Bound _) = mempty
    foldFreesOcc f c (Free v)  = foldFreesOcc f c v

    mapFrees _ b@(Bound _) = pure b
    mapFrees f   (Free v)  = Free <$> mapFrees f v

instance (HasFrees l, Ord l) => HasFrees (Term l) where
    foldFrees f = foldMap (foldFrees f)

    foldFreesOcc f c t = case viewTerm t of
        Lit  l             -> foldFreesOcc f c l
        FApp (NoEq o) as -> foldFreesOcc f ((BC.unpack . fst $ o):c) as
        FApp o        as -> mconcat $ map (foldFreesOcc f (show o:c)) as
          -- AC or C symbols

    mapFrees f (viewTerm -> Lit l)                  = lit <$> mapFrees f l
    mapFrees f@(Arbitrary _) (viewTerm -> FApp o l) = fApp o <$> mapFrees f l
    mapFrees f@(Monotone _)  (viewTerm -> FApp o l) = unsafefApp o <$> mapFrees f l

instance HasFrees a => HasFrees (Equal a) where
    foldFrees    f               = foldMap (foldFrees f)
    foldFreesOcc f p (Equal a b) = foldFreesOcc f p (a,b)
    mapFrees     f               = traverse (mapFrees f)

instance HasFrees a => HasFrees (Match a) where
    foldFrees    f                       = foldMap (foldFrees f)
    foldFreesOcc _ _ NoMatch             = mempty
    foldFreesOcc f p (DelayedMatches ms) = foldFreesOcc f p ms
    mapFrees     f                       = traverse (mapFrees f)

instance HasFrees a => HasFrees (RRule a) where
    foldFrees    f               = foldMap (foldFrees f)
    foldFreesOcc f p (RRule a b) = foldFreesOcc f p (a,b)
    mapFrees     f               = traverse (mapFrees f)

instance HasFrees () where
    foldFrees    _   = const mempty
    foldFreesOcc _ _ = const mempty
    mapFrees     _   = pure

instance HasFrees Int where
    foldFrees    _   = const mempty
    foldFreesOcc _ _ = const mempty
    mapFrees     _   = pure

instance HasFrees Integer where
    foldFrees    _   = const mempty
    foldFreesOcc _ _ = const mempty
    mapFrees     _   = pure

instance HasFrees Bool where
    foldFrees    _   = const mempty
    foldFreesOcc _ _ = const mempty
    mapFrees     _   = pure

instance HasFrees Char where
    foldFrees    _   = const mempty
    foldFreesOcc _ _ = const mempty
    mapFrees     _   = pure

instance HasFrees a => HasFrees (Maybe a) where
    foldFrees    f            = foldMap (foldFrees f)
    foldFreesOcc _ _ Nothing  = mempty
    foldFreesOcc f p (Just x) = foldFreesOcc f p x
    mapFrees     f            = traverse (mapFrees f)

instance (HasFrees a, HasFrees b) => HasFrees (Either a b) where
    foldFrees    f   = either (foldFrees f) (foldFrees f)
    foldFreesOcc f p = either (foldFreesOcc f ("0":p)) (foldFreesOcc f ("1":p))
    mapFrees     f   = either (fmap Left . mapFrees   f) (fmap Right . mapFrees   f)

instance (HasFrees a, HasFrees b) => HasFrees (a, b) where
    foldFrees    f   (x, y) = foldFrees f x `mappend` foldFrees f y
    foldFreesOcc f p (x, y) = foldFreesOcc f ("0":p) x `mappend` foldFreesOcc f ("1":p) y
    mapFrees     f   (x, y) = (,) <$> mapFrees   f x <*> mapFrees   f y

instance (HasFrees a, HasFrees b, HasFrees c) => HasFrees (a, b, c) where
    foldFrees    f (x, y, z)    = foldFrees f (x, (y, z))
    foldFreesOcc f p (x, y, z)  =
        foldFreesOcc f ("0":p) x `mappend` foldFreesOcc f ("1":p) y `mappend` foldFreesOcc f ("2":p) z
    mapFrees     f (x0, y0, z0) =
        (\(x, (y, z)) -> (x, y, z)) <$> mapFrees f (x0, (y0, z0))

instance HasFrees a => HasFrees [a] where
    foldFrees    f      = foldMap  (foldFrees f)
    foldFreesOcc f c xs = mconcat $ (map (\(i,x) -> foldFreesOcc f (show i:c) x)) $ zip [(0::Int)..] xs
    mapFrees     f      = traverse (mapFrees f)

instance HasFrees a => HasFrees (Disj a) where
    foldFrees    f     = foldMap  (foldFrees f)
    foldFreesOcc f p d = foldFreesOcc f p (getDisj d)
    mapFrees     f     = traverse (mapFrees f)

instance HasFrees a => HasFrees (Conj a) where
    foldFrees    f     = foldMap  (foldFrees f)
    foldFreesOcc f p c = foldFreesOcc f p (getConj c)
    mapFrees     f     = traverse (mapFrees f)

instance (Ord a, HasFrees a) => HasFrees (S.Set a) where
    foldFrees   f    = foldMap  (foldFrees f)
    foldFreesOcc f p = foldMap (foldFreesOcc f ("0":p))
    mapFrees     f   = fmap S.fromList . mapFrees f . S.toList

instance (Ord k, HasFrees k, HasFrees v) => HasFrees (M.Map k v) where
    foldFrees f = M.foldrWithKey combine mempty
      where
        combine k v m = foldFrees f k `mappend` (foldFrees f v `mappend` m)
    foldFreesOcc f p = M.foldrWithKey combine mempty
      where
        combine k v m = foldFreesOcc f p (k,v) `mappend` m
    mapFrees f = fmap M.fromList . mapFrees f . M.toList


------------------------------------------------------------------------------
-- Pretty Printing
------------------------------------------------------------------------------

-- | Pretty print a 'LVar'.
prettyLVar :: Document d => LVar -> d
prettyLVar = text . show

-- | Pretty print a 'NodeId'.
prettyNodeId :: Document d => NodeId -> d
prettyNodeId = text . show

-- | Pretty print an @NTerm@.
prettyNTerm :: (Show v, Document d) => NTerm v -> d
prettyNTerm = prettyTerm (text . show)

-- | Pretty print an @LTerm@.
prettyLNTerm :: Document d => LNTerm -> d
prettyLNTerm = prettyNTerm


-- derived instances
--------------------

$( derive makeBinary ''NameTag)
$( derive makeBinary ''Name)
$( derive makeBinary ''LSort)
$( derive makeBinary ''LVar)
$( derive makeBinary ''BVar)

$( derive makeNFData ''NameTag)
$( derive makeNFData ''Name)
$( derive makeNFData ''LSort)
$( derive makeNFData ''LVar)
$( derive makeNFData ''BVar)