-- |
-- 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 ((forall x. Ignore t -> Rep (Ignore t) x)
-> (forall x. Rep (Ignore t) x -> Ignore t) -> Generic (Ignore t)
forall x. Rep (Ignore t) x -> Ignore t
forall x. Ignore t -> Rep (Ignore t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Ignore t) x -> Ignore t
forall t x. Ignore t -> Rep (Ignore t) x
$cfrom :: forall t x. Ignore t -> Rep (Ignore t) x
from :: forall x. Ignore t -> Rep (Ignore t) x
$cto :: forall t x. Rep (Ignore t) x -> Ignore t
to :: forall x. Rep (Ignore t) x -> Ignore t
Generic)

instance (NFData t) => NFData (Ignore t) where
    rnf :: Ignore t -> ()
rnf (I t
t) = t -> ()
forall a. NFData a => a -> ()
rnf t
t () -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance (Show t) => Show (Ignore t) where
    showsPrec :: Int -> Ignore t -> ShowS
showsPrec Int
prec (I t
t) = 
        Bool -> ShowS -> ShowS
showParen (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (String -> ShowS
showString String
"<-" 
                              ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> t -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
prec t
t
                              ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"->")

instance (Show t) => Alpha (Ignore t) where
    aeq' :: AlphaCtx -> Ignore t -> Ignore t -> Bool
aeq' AlphaCtx
_ Ignore t
_ Ignore t
_ = Bool
True
    fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ignore t -> f (Ignore t)
fvAny' AlphaCtx
_ AnyName -> f AnyName
_ = Ignore t -> f (Ignore t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    isPat :: Ignore t -> DisjointSet AnyName
isPat Ignore t
_ = DisjointSet AnyName
forall a. DisjointSet a
inconsistentDisjointSet
    isTerm :: Ignore t -> All
isTerm Ignore t
_ = All
forall a. Monoid a => a
mempty
    close :: AlphaCtx -> NamePatFind -> Ignore t -> Ignore t
close AlphaCtx
_ NamePatFind
_ = Ignore t -> Ignore t
forall a. a -> a
id
    open :: AlphaCtx -> NthPatFind -> Ignore t -> Ignore t
open AlphaCtx
_ NthPatFind
_ = Ignore t -> Ignore t
forall a. a -> a
id
    namePatFind :: Ignore t -> NamePatFind
namePatFind  Ignore t
_ = (AnyName -> Either Integer Integer) -> NamePatFind
NamePatFind ((AnyName -> Either Integer Integer) -> NamePatFind)
-> (AnyName -> Either Integer Integer) -> NamePatFind
forall a b. (a -> b) -> a -> b
$ Either Integer Integer -> AnyName -> Either Integer Integer
forall a b. a -> b -> a
const (Either Integer Integer -> AnyName -> Either Integer Integer)
-> Either Integer Integer -> AnyName -> Either Integer Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Either Integer Integer
forall a b. a -> Either a b
Left Integer
0
    nthPatFind :: Ignore t -> NthPatFind
nthPatFind Ignore t
_ = (Integer -> Either Integer AnyName) -> NthPatFind
NthPatFind Integer -> Either Integer AnyName
forall a b. a -> Either a b
Left
    swaps' :: AlphaCtx -> Perm AnyName -> Ignore t -> Ignore t
swaps' AlphaCtx
_ Perm AnyName
_ = Ignore t -> Ignore t
forall a. a -> a
id
    lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ignore t -> (Ignore t -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
_ Ignore t
i Ignore t -> Perm AnyName -> m b
cont = Ignore t -> Perm AnyName -> m b
cont Ignore t
i Perm AnyName
forall a. Monoid a => a
mempty
    freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ignore t -> m (Ignore t, Perm AnyName)
freshen' AlphaCtx
_ Ignore t
i = (Ignore t, Perm AnyName) -> m (Ignore t, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ignore t
i, Perm AnyName
forall a. Monoid a => a
mempty)
    acompare' :: AlphaCtx -> Ignore t -> Ignore t -> Ordering
acompare' AlphaCtx
_ Ignore t
_ Ignore t
_ = Ordering
EQ