Zabt

Abstract binding trees with a nameless internal representation.

Documentation

data Term v f

An abstract Term v f is an abstract binding tree of the shape described by the pattern functor f augmented with variables named by v. Equality is alpha-equivalence. In particular, Term v f is (morally) equivalent to the fixed-point of the pattern-algebra View respecting the binding properties of VLam and VVar.

Instances

(Eq v, Eq (f (Term v f))) => Eq (Term v f)

Methods

(==) :: Term v f -> Term v f -> Bool

(/=) :: Term v f -> Term v f -> Bool

(Ord v, Ord (f (Term v f))) => Ord (Term v f)

Methods

compare :: Term v f -> Term v f -> Ordering

(<) :: Term v f -> Term v f -> Bool

(<=) :: Term v f -> Term v f -> Bool

(>) :: Term v f -> Term v f -> Bool

(>=) :: Term v f -> Term v f -> Bool

max :: Term v f -> Term v f -> Term v f

min :: Term v f -> Term v f -> Term v f

(Show v, Show (Nameless v f (Term v f))) => Show (Term v f)

Methods

showsPrec :: Int -> Term v f -> ShowS

show :: Term v f -> String

showList :: [Term v f] -> ShowS

pattern Var :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => v -> Term v f

Var v creates and matches a Term value corresponding to a free variable.

pattern Lam :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => v -> Term v f -> Term v f

Lam v t creates and matches a Term value where the free variable v has been abstracted over, becoming bound.

pattern Pat :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => f (Term v f) -> Term v f

Pat f creates and matches a Term value built from a layer of the pattern functor f.

subst :: (Foldable f, Functor f, Ord v) => Map v (Term v f) -> Term v f -> Term v f

Substitute some free variables.

subst1 :: (Foldable f, Ord v, Functor f) => (v, Term v f) -> Term v f -> Term v f

Substitute just one free variable.

freeVars :: Term v f -> Set v

Returns the free variables used within a given Term.

NOTE: We have to define a new function in order to not accidentally break encapsulation. Just exporting free direction would allow uses to manipulate the Term value and break invariants (!).

data View v f x

A concrete view of the top "layer" of a Term ABT. This top layer may be an abstraction, a raw variable, or a branch of the pattern functor f. Normally View is wrapping a Term value, the abstract "remainder" of the tree.

Constructors

VVar v

VLam v x

VPat (f x)

Instances

Functor f => Functor (View v f)

Methods

fmap :: (a -> b) -> View v f a -> View v f b

(<$) :: a -> View v f b -> View v f a

(Eq v, Eq x, Eq (f x)) => Eq (View v f x)

Methods

(==) :: View v f x -> View v f x -> Bool

(/=) :: View v f x -> View v f x -> Bool

(Show v, Show x, Show (f x)) => Show (View v f x)

Methods

showsPrec :: Int -> View v f x -> ShowS

show :: View v f x -> String

showList :: [View v f x] -> ShowS

fold :: (Functor f, Foldable f, Ord v) => View v f (Term v f) -> Term v f

Construct a Term from one layer of a View.

unfold :: (Functor f, Foldable f, Ord v, Freshen v) => Term v f -> View v f (Term v f)

Strip the top layer of a View off of a Term.

class Eq v => Freshen v where

A type which can be freshened has an operation which attempts to find a unique version of its input. The principal thing that must hold is that `freshen n /= n`. It's not necessary that `freshen n` be totally fresh with respect to a context---that's too much to ask of a value---but it is necessary that freshen *eventually* produces a fresh value.

Minimal complete definition

freshen

Methods

freshen :: v -> v

Instances

Freshen Int

Methods

freshen :: Int -> Int