Zabt.Internal.Term

Documentation

data Term v f a

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

Constructors

Term

Fields

• free :: Set v
• project :: Nameless v f (Term v f) a

Instances

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

Methods

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

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

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

Methods

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

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

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

Methods

compare :: Term v f (B a) -> Term v f (B a) -> Ordering

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

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

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

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

max :: Term v f (B a) -> Term v f (B a) -> Term v f (B a)

min :: Term v f (B a) -> Term v f (B a) -> Term v f (B a)

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

Methods

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

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

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

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

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

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

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

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

Methods

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

show :: Term v f a -> String

showList :: [Term v f a] -> ShowS

type Flat v f = Term v f G

A Flat Term is one which is not immediately binding any variables.

freeVars :: Term v f a -> 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, Visits f) => Nameless v f (Term v f) a -> Term v f a

var :: (Visits f, Ord v) => v -> Flat v f

abstract :: forall v f a. (Visits f, Ord v) => v -> Term v f a -> Term v f a

substitute :: forall v f a. (Visits f, Ord v) => v -> Term v f a -> Term v f a

substitute' :: forall v f a. (Visits f, Ord v) => Flat v f -> Term v f a -> Term v f a

subst :: forall v f a. (Visits f, Ord v) => (v -> Maybe (Flat v f)) -> Term v f a -> Term v f a

Substitute some free variables.

substMap :: forall v f a. (Visits f, Ord v) => Map v (Flat v f) -> Term v f a -> Term v f a

Substitute some free variables from a finite map.

subst1 :: forall v f a. (Visits f, Ord v) => (v, Flat v f) -> Term v f a -> Term v f a

Substitute just one free variable.