Zabt.Internal.Term

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 VAbs and VVar.

Constructors

Term

Fields

• free :: Set v
• project :: 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

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

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

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

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

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

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

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.