module Zabt.Internal.Nameless where
import GHC.Show (showSpace)
import Zabt.Arity
import Zabt.Internal.Index
data Nameless v (f :: (Arity -> *) -> *) (x :: Arity -> *) (a :: Arity) where
Free :: !v -> Nameless v f x G
Bound :: !Index -> Nameless v f x G
Pattern :: f x -> Nameless v f x G
Abstraction :: !v -> x a -> Nameless v f x (B a)
instance (Show v, Show (x G), Show (f x)) => Show (Nameless v f x G) where
showsPrec p (Free v) = showsPrec 11 v
showsPrec p (Bound i) = showString "'" . showsPrec 11 i
showsPrec p (Pattern f) = showsPrec p f
instance (Show v, Show (x a), Show (f x)) => Show (Nameless v f x (B a)) where
showsPrec p (Abstraction v t) = showParen (p >= 11) $
showString "λ"
. showSpace
. showsPrec 11 t
instance (Eq v, Eq (f x)) => Eq (Nameless v f x G) where
Free va == Free vb = va == vb
Bound ixa == Bound ixb = ixa == ixb
Pattern fa == Pattern fb = fa == fb
_ == _ = False
instance (Eq (x a), Eq (f x)) => Eq (Nameless v f x (B a)) where
Abstraction _ ta == Abstraction _ tb = ta == tb
_ == _ = False
instance (Ord v, Ord (f x)) => Ord (Nameless v f x G) where
Free va `compare` Free vb = va `compare` vb
Bound ixa `compare` Bound ixb = ixa `compare` ixb
Pattern fa `compare` Pattern fb = fa `compare` fb
instance (Ord v, Ord (x a), Ord (f x)) => Ord (Nameless v f x (B a)) where
Abstraction _ ta `compare` Abstraction _ tb = ta `compare` tb