module Zabt.View where
import GHC.Show
import Zabt.Freshen
import Zabt.Internal.Nameless
import Zabt.Internal.Term
data View v f x
= VVar !v
| VPat (f x)
| VAbs !v x
deriving (Eq, Ord)
instance (Show v, Show x, Show (f x)) => Show (View v f x) 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
showsPrec p (VAbs v t) = showParen (p >= 11) $
showString "VAbs "
. showsPrec 11 v
. showSpace
. showsPrec 11 t
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 :: (Foldable f, Functor f, Ord v) => View v f (Term v f) -> Term v f
fold v = case v of
VVar v -> var v
VAbs v t -> embed (Abstraction (Scope v (abstract v t)))
VPat f -> embed (Pattern f)
unfold :: (Foldable f, Functor f, Ord v, Freshen v) => Term v f -> View v f (Term v f)
unfold t =
case project t of
Free v -> VVar v
Bound _idx -> error "naked bound variable, invariant broken!"
Abstraction (Scope v t') ->
let v' = freshWrt (free t) v in
VAbs v' (substitute v' t')
Pattern f -> VPat f