module Zabt.View where
import GHC.Show
import Zabt.Arity
import Zabt.Freshen
import Zabt.Internal.Nameless
import Zabt.Internal.Term
import Zabt.Visits
data View v (f :: (Arity -> *) -> *) (x :: Arity -> *) (a :: Arity) where
VVar :: !v -> View v f x G
VPat :: f x -> View v f x G
VAbs :: !v -> x a -> View v f x (B a)
instance (Show v, Show (x G), Show (f x)) => Show (View v f x G) where
showsPrec p (VVar v) = showParen (p >= 11) $ showString "VVar " . showsPrec 11 v
showsPrec p (VPat f) = showParen (p >= 11) $ showString "VPat " . showsPrec 11 f
instance (Show v, Show (x a), Show (f x)) => Show (View v f x (B a)) where
showsPrec p (VAbs v t) = showParen (p >= 11) $
showString "VAbs "
. showsPrec 11 v
. showSpace
. showsPrec 11 t
instance (Eq v, Eq (f x)) => Eq (View v f x G) where
VVar va == VVar vb = va == vb
VPat fa == VPat fb = fa == fb
instance (Eq (x a), Eq (f x)) => Eq (View v f x (B a)) where
VAbs _ ta == VAbs _ tb = ta == tb
instance (Ord v, Ord (f x)) => Ord (View v f x G) where
VVar va `compare` VVar vb = va `compare` vb
VPat fa `compare` VPat fb = fa `compare` fb
instance (Ord v, Ord (x a), Ord (f x)) => Ord (View v f x (B a)) where
VAbs _ ta `compare` VAbs _ tb = ta `compare` tb
pattern Var a <- (unfold -> VVar a) where
Var a = fold (VVar a)
pattern Abs v t <- (unfold -> VAbs v t) where
Abs v t = fold (VAbs v t)
pattern Pat f <- (unfold -> VPat f) where
Pat f = fold (VPat f)
fold :: (Visits f, Ord v) => View v f (Term v f) a -> Term v f a
fold v = case v of
VVar v -> var v
VAbs v t -> embed (Abstraction v (abstract v t))
VPat f -> embed (Pattern f)
unfold :: (Visits f, Ord v, Freshen v) => Term v f a -> View v f (Term v f) a
unfold t =
case project t of
Free v -> VVar v
Bound _idx -> error "naked bound variable, invariant broken!"
Abstraction v t' ->
let v' = freshWrt (free t) v in
VAbs v' (substitute v' t')
Pattern f -> VPat f