Zabt

Abstract binding trees with a nameless internal representation.

Abstract binding tree terms

Abstract binding trees take the form Term v f a, or, more commonly, Flat v f. These types are abstract—you will never construct or analyze them directly.

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 VAbs 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

Constructing terms with View patterns

To construct or analyze a Term, the Var, Abs, and Pat pattern synonyms are useful. These synonyms let you essentially treat Term as if it weren't abstract and both construct new terms and case analyze them.

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 Abs :: forall f v. (Freshen v, Foldable f, Ord v, Functor f) => v -> Term v f -> Term v f

Abs 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.

Working with free variables

Abstract binding trees take the form Term v f a, or, more commonly, Flat v f. These types are abstract---you will never construct or analyze them directly.

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

Substitute some free variables.

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

Substitute some free variables from a finite map.

subst1 :: (Functor f, Foldable f, Ord v) => (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 (!).

Freshen class

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.

Variable identifier types must be instances of Freshen.

Minimal complete definition

freshen

Methods

freshen :: v -> v

Instances

Freshen Int

Methods

freshen :: Int -> Int

Freshen Index

Methods

freshen :: Index -> Index

Freshen Name

Methods

freshen :: Name -> Name

View in detail

data View v f x

Constructors

VVar !v

VPat (f x)

VAbs !v x

Instances

(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

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

Methods

compare :: View v f x -> View v f x -> Ordering

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

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

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

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

max :: View v f x -> View v f x -> View v f x

min :: View v f x -> View v f x -> View v f x

(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 :: (Foldable f, Functor f, Ord v) => View v f (Term v f) -> Term v f

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