content: -- |
  -- Module     : Unbound.Generics.LocallyNameless.Ignore
  -- Copyright  : (c) 2018, Reed Mullanix
  -- License    : BSD3 (See LICENSE)
  -- Maintainer : Reed Mullanix
  -- Stability  : experimental
  --
  -- Ignores a term for the purposes of alpha-equality and substitution
  {-# LANGUAGE DeriveGeneric #-}
  module Unbound.Generics.LocallyNameless.Ignore (
      Ignore(..)
      ) where
  
  import Control.DeepSeq (NFData(..))
  import Control.Applicative
  import Data.Monoid 
  
  import GHC.Generics (Generic)
  
  import Unbound.Generics.LocallyNameless.Alpha
  
  -- | Ignores a term 't' for the purpose of alpha-equality and substitution
  data Ignore t = I !t
          deriving (Generic)
  
  instance (NFData t) => NFData (Ignore t) where
      rnf (I t) = rnf t `seq` ()
  
  instance (Show t) => Show (Ignore t) where
      showsPrec prec (I t) = 
          showParen (prec > 0) (showString "<-" 
                                . showsPrec prec t
                                . showString "->")
  
  instance (Show t) => Alpha (Ignore t) where
      aeq' _ _ _ = True
      fvAny' _ _ = pure
      isPat _ = inconsistentDisjointSet
      isTerm _ = mempty
      close _ _ = id
      open _ _ = id
      namePatFind  _ = NamePatFind $ const $ Left 0
      nthPatFind _ = NthPatFind Left
      swaps' _ _ = id
      lfreshen' _ i cont = cont i mempty
      freshen' _ i = return (i, mempty)
      acompare' _ _ _ = EQ