Zabt.Internal

Internal module, expert use only. Using this module allows you to easily break ABT invariants and generally have a terrible, no good, really bad time.

Documentation

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

freshPred :: Freshen v => (v -> Bool) -> v -> v

freshSet :: (Ord v, Freshen v) => Set v -> v -> v

data Nameless v f x

The Nameless algebra describes one layer of a nameless representation of a binding tree parameterzed by another pattern algebra, f, which does not make reference to variable binding.

Constructors

F v

B Int

Abst v x

Branch (f x)

Instances

Functor f => Functor (Nameless v f)

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

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

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

max :: Nameless v f x -> Nameless v f x -> Nameless v f x

min :: Nameless v f x -> Nameless v f x -> Nameless v f x

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

Methods

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

show :: Nameless v f x -> String

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

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.

Constructors

Term

Fields

• free :: Set v
• open :: Nameless v f (Term v f)

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

close :: (Ord v, Foldable f) => Nameless v f (Term v f) -> Term v f

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

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.

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.

_var :: v -> Term v f

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

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

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 (!).

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.